turnstone/HYPOTHESIS.md

What is a harness?

A hypothesis — not a theorem. The honest answer is a claim about shape: an object you can write down that says what a harness is and, just as precisely, the guarantee it cannot carry for free.

Most descriptions of an agent framework are a feature list. This is an attempt at a definition.

---

The claim

Informal. A harness is a stopped, deterministically-controlled Markov process on task-state, closed around a stopped autoregressive process on context-space, driven by a learned model kernel — a deterministic controller in closed loop with a stochastic learned plant.

In plain terms. The harness is the whole governed loop: a deterministic shell you write — build the prompt, authorize an action, fold the response back into state — wrapped around a black-box stochastic model kernel (the plant, M_W) and the environment its actions touch, looped until it halts in H. The shell is deterministic, M_W is not, and everything below makes that split precise.

Formal — the objects. A harness is a tuple \mathcal{H} = (\mathcal{S}, \mathcal{C}, \mathcal{Y}, \mathcal{A}, \mathcal{E}, \pi, M_W, \gamma, Q_E, \rho, H, H_{\mathrm{ok}}, B, \mu_0) over standard Borel spaces (concretely: the controlled state is standard Borel by construction — token sequences, finite config maps, bounded counters and ledgers, finite tuples of real vectors — and the model/environment coordinates are inherited as such whenever they serialize to a Polish space; the assumption is roomier than it looks — even a belief-state coordinate valued in \mathcal{P}(X) survives, since \mathcal{P}(X) is Polish for Polish X — and fails only for a genuinely non-separable coordinate, an uncountable product $\sigma$-algebra being the canonical hazard, which this construction avoids): a deterministic lowering \pi:\mathcal{S}\to\mathcal{C}; a stochastic model-run kernel M_W(c, dy) into a readout space \mathcal{Y} (which includes the parse-failure \bot_{\mathcal{Y}}, so M_W and \gamma are total over it); a deterministic authorization gate \gamma:\mathcal{S}\times\mathcal{Y}\to\mathcal{A}_{\bot} that validates the model's parsed readout into an authorized action in \mathcal{A} or rejects it as \bot_{\mathcal{A}} (parsing itself lives inside M_W — realized as the readout R of the specialization below); a stochastic environment/tool kernel Q_E:\mathcal{S}\times\mathcal{A}_{\bot}\rightsquigarrow\mathcal{E} on the authorized action (rejection included, with Q_E(s,\bot,\cdot)=\delta_{e_0} for a distinguished no-op response e_0\in\mathcal{E}); and a deterministic verify-and-fold-back map \rho:\mathcal{S}\times\mathcal{Y}\times\mathcal{A}_{\bot}\times\mathcal{E}\to\mathcal{S}; and an initial law \mu_0 on \mathcal{S} (carried in the tuple, not free — the determinism claim C2 is conditional on a fixed s_0, and left to vary \mu_0 is itself a coin). Three measurability requirements make the objects well-defined rather than merely typed: every map (\pi,\gamma,\rho, the halt test, and c\mapsto M_W(c,\cdot), (s,a)\mapsto Q_E(s,a,\cdot) as kernels) is Borel measurable, and the sets H, H_{\mathrm{ok}}, B are Borel. And the rejection symbol is really two: the parse failure \bot_{\mathcal{Y}}\in\mathcal{Y} that M_W can emit (the readout could not be formed) is distinct from the authorization rejection \bot_{\mathcal{A}}\in\mathcal{A}_{\bot} that \gamma can return (a well-formed readout was refused) — both force the no-op response e_0, but they are different events with different downstream readings, and collapsing them onto one \bot hides a proposal that parsed-and-was-refused behind one that never parsed. Two conventions ride on the split: \gamma(s,\bot_{\mathcal{Y}})=\bot_{\mathcal{A}} is an axiom — a readout that never formed can never authorize, and it is how parse failure reaches the no-op at all, since Q_E accepts only \mathcal{A}_{\bot}; and an unsubscripted \bot elsewhere reads by position — \bot_{\mathcal{A}} in $\gamma$'s output and $Q_E$'s input, \bot_{\mathcal{Y}} where a readout fails to parse.

Terminal structure. The terminal set is an absorbing halt set H\subseteq\mathcal{S} (the daemon "ready-state" recurrence of the note below is a separate, non-absorbing object) with accepting subset H_{\mathrm{ok}}\subseteq H — read as operational acceptance H_{\mathrm{acc}}, the halts the controller declares accepted, which is all an implementation can test; genuine extensional success G\subseteq H is a separate, analysis-only set that need not be computable (the semantic-adequacy gap of this document is exactly H_{\mathrm{acc}}\setminus G, a well-formed halt the shell accepts that is nonetheless wrong), and the two coincide only when correctness is decidable by the shell, which natural-language tasks deny. The convention hereafter: operational statements — fail-closed, the ledger, the failure set F — read H_{\mathrm{ok}} as H_{\mathrm{acc}}; success and wall claims (p_{\mathrm{succ}} as accuracy, V^\star_{\mathrm{ok}}, C5 and C6) read it against G, with H_{\mathrm{acc}}=G assumed on evaluation families an external judge scores — absent that assumption, a shell that rubber-stamps acceptance beats any ceiling vacuously. Separately, a bad set B\subseteq\mathcal{S} (B\cap H_{\mathrm{ok}}=\varnothing) marks the unsafe states for reach-avoid, possibly entered before any halt; hitting times are \tau_A=\inf\{n\ge 0:s_n\in A\}, and \tau_H is a stopping time for the natural filtration.

The outer kernel. The induced outer transition kernel, for s\notin H, is

T(s, A) = \int_{\mathcal{Y}}\!\int_{\mathcal{E}} \mathbf{1}_A\!\big(\rho(s, y, \gamma(s,y), e)\big)\; Q_E\big(s, \gamma(s,y), de\big)\; M_W(\pi(s), dy), \qquad T(s,A)=\mathbf{1}_A(s)\ \text{ for } s\in H,

and the harness runs s_{n+1} \sim T(s_n) from an initial s_0 \sim \mu_0 until \tau_H = \inf\{n : s_n \in H\}. Because \pi, \gamma, \rho, H are deterministic they contribute no integration variable of their own — they appear as measurable transformations inside the integrand (the pushforward), not literally outside it — so the controller injects no randomness, and every coin is inherited from M_W and Q_E. (The earlier shorthand T = \rho \circ (M_W \circ \pi, E) is suggestive but ill-typed — M_W returns a law, while \rho consumes a sample together with the prior state s; the integral is what the shorthand meant.) One typing subtlety the displayed form hides, and the chokepoint claim depends on it: writing Q_E(s,a) lets the environment read all of s — including secrets and prior model output \rho folded in, which would be a delayed model-to-world path y_n \to s_{n+1} \to Q_E that never re-crossed \gamma. The intended reading factors the state, s=(q,w) with q controller-observable and w possibly-latent world state, and restricts the tool kernel to Q_E(w, a): the environment sees only the world and the authorized, capability-scoped action, so anything from q the tool needs must be placed inside $a$, after authorization. The factorization retypes the kernel's output as well, and has to: Q_E becomes a kernel (w,a)\rightsquigarrow(w',o) — the actual next world together with the observed receipt — and \rho acts as \rho\big((q,w),y,a,(w',o)\big)=(\rho_q(q,y,a,o),\,w'), folding only the receipt into controller state while the world writes itself; the displayed T, in which \rho appears to manufacture the entire next state from e, is the unfactored shorthand — read e=(w',o) with \rho_q blind to the w' coordinate — for if \rho computed the world from the receipt, the ledger would be true by construction and the reported-vs-actual gap of Reading it could not exist. Under that factorization B is properly a subset of the global (q,w), and \gamma is genuinely the only channel from model output into the world; the single-symbol s elsewhere in this document is shorthand for q wherever a controller map reads it, for w alone where Q_E reads it, and for (q,w) wherever reach-avoid is evaluated.

Fail-closed. The gate \gamma is what makes fail-closed a property, not just a name: model output is an untrusted proposal, and \gamma(s,y)=\bot forces a no-op environment response (Q_E(s,\bot,\cdot)=\delta_{e_0}) — so a malformed or unauthorized tool call is rejected before it can act, not validated after its side effects have landed. Fail-closed is then the property that a rejected proposal causes no unauthorized side effect and lands in a safe, non-bad set — but quantified honestly it holds only from already-safe states, so the sharp form names a rejection-invariant safe set K with s\in K,\ \gamma(s,y)=\bot_{\mathcal{A}} \Rightarrow \rho(s,y,\bot_{\mathcal{A}},e_0)\in K (and K\cap B=\varnothing): a rejection from inside K stays inside K, landing in a non-accepting terminal H\setminus H_{\mathrm{ok}} in the strict case or a safe non-terminal state when the spec retries. Fail-closed is closure of K under rejection, not a claim that rejection rescues a state already in B. And \rho must validate the tool response e, not only the proposal that \gamma already gated: a malformed or adversarial response e is caught at fold-back, not just at the gate. But response-validation has a hard limit: \rho can reject a bad tool response, yet it cannot undo side effects an authorized action already caused — so \gamma, not \rho, is the last line before irreversible effects, and anything irreversible must be gated at authorization. The boundary is also only real if raw model output reaches no sink — tool, logger, browser, or remote call — before \gamma; any pre-authorization escape bypasses the gate. The user-visible final response and any logging are themselves effects, and the rule binds model-authored bytes: they reach a sink either as an authorized action through \gamma, or only after an accepted halt in H_{\mathrm{ok}}. Shell-templated text — a refusal notice, a cancellation report reading the ledger — is controller output, outside $\gamma$'s jurisdiction, and may accompany any halt (a template that interpolates model-authored fragments inherits the model's label — the appendix's meet rule — and those bytes are gated like any others); the invariant is that raw model text never reaches a sink ungated, not that failed runs die silent.

The harness invariants. These are the invariants that make \mathcal{H} a harness and not merely a controlled Markov process with a learned kernel inside: the model sees only \mathcal{C}, never full \mathcal{S}; its outputs are proposals, not actions; a deterministic capability boundary \gamma gates every side effect; and the terminal set H splits into accepting (H_{\mathrm{ok}}) and non-accepting (H\setminus H_{\mathrm{ok}} — safe refusals outside B, and wrong or bad halts possibly in B), while the bad set B is a separate unsafe set — possibly absorbing, possibly entered mid-run before any halt — against which \tau_B is measured for reach-avoid. Two notes keep the invariants honest. They are signature, not strength: a \gamma that authorizes everything still satisfies the tuple, as a trivial group satisfies the group axioms — the definition admits degenerate harnesses, and fail-closed, provenance isolation, and the certificates below are properties a particular harness earns, not gifts of the signature. And the first invariant has a sharper, two-sided form: \pi is the only channel from state to model — the confidentiality floor lives at what \pi must never lower (credentials, other principals' data) — exactly as \gamma is the only channel from model output to effect, where the injection bounds live; exfiltration is therefore cut at either chokepoint, never lowered or never emitted (the gate refusing the read whose URL is the payload is the emission-side cut). One chokepoint out of the state, one into the world; a bypass of either is the same bug with the sign flipped. A caution on what the tuple alone settles: it is a normal form, not yet a discriminating definition — almost any Markov kernel fits it by pushing all randomness into M_W, authorizing everything at \gamma, and letting \rho return the sampled next state, and "learned" is nowhere formalized. What discriminates a harness is the causal architecture these invariants describe together with a realizability condition: an implementation realizes the normal form only if it has no channel the diagram omits — no path from model output to an effect except through \gamma, no input to a controller map the diagram does not show. The determinism and gate claims below (C1, C3) are therefore properties of an implementation that realizes the contract, checked by the falsifiers, not gifts of writing the tuple down; a diagram is not its referent.

Beyond the stationary kernel. This displayed T is the time-homogeneous, fixed-kernel case; for nonstationary or adversarial environments, replace Q_E with a time-indexed kernel Q_{E,n} — or an admissible family of kernels, or an adversary's policy — over which the robust certificate (the minimax form under The limit) quantifies. If that adversary conditions on history rather than only the current (s, y), the history must itself live in s — otherwise the object is a Markov game requiring further augmentation, not a Markov chain. And nonstationarity is not the environment's monopoly: a provider retraining or re-serving under a fixed endpoint name is a nonstationary M_{W,n} — the table places model version in s precisely so a version bump is a visible state change — and any measured surrogate (the \delta of The limit) is calibrated against one kernel and dies with the bump; the dashboard must be keyed to the kernel it measured.

The inner kernel. M_W is itself a stopped process, and for a decoder-only transformer it is implemented as

M_W(c, \cdot) = \mathrm{Law}\big(R(z_{\tau})\big), \quad z_t = (c_t, b_t, m_t), \quad v \sim K_W(c_t, \cdot), \quad K_W(c, v) = (U \circ \Phi_W \circ \mathrm{Emb})(c)[v], \quad c_{t+1} = \mathrm{suffix}_{\le L}(c_t\!\cdot\! v),\ \ b_{t+1} = b_t\!\cdot\! v,\ \ m_{t+1} = \mathsf{step}(m_t, v),\ \ \tau=\inf\{t:m_t\in\mathrm{Stop}\}.

with the layer stack \Phi_W on the residual stream as the (loosely) "manifold" core — formally just the learned high-dimensional residual-stream transformation, with manifold-proper reserved for the frontier. The inner state z_t=(c_t,b_t,m_t) separates the model-visible window c_t (the \le L slice that slides) from the untruncated output buffer b_t (the transcript the readout actually consumes, so truncation never loses it) and the parser/stop state m_t (parser state, a token counter, and a clock, so the cap and timeout are functions of it), updated m_{t+1}=\mathsf{step}(m_t,v), whose stop set \mathrm{Stop} — EOS emitted, max-token cap, timeout, or parse-failure \bot — forces \tau=\inf\{t:m_t\in\mathrm{Stop}\} finite, making M_W a genuine probability kernel rather than a sub-probability one completed by a cemetery output. (One honesty note on the clock: a token-count cap is a deterministic function of the run, but a wall-clock timeout imports infrastructure noise — server load, batching, congestion — into the kernel's coin; legitimate, a kernel may carry any randomness, but it makes the displayed M_W the model plus its serving substrate, and the determinism audit under How this could be wrong must hold the clock fixed along with the samples.) The readout is total, R : \mathcal{Z} \to \mathcal{Y} — a parsed tool-call, answer, or transcript, returning the parse-failure \bot\in\mathcal{Y} when parsing fails; crucially R is a syntactic, verified readout (parsing and extraction), not a semantic solver, or the $L$-wall below is void — arbitrary computation could hide in R off the \le L window — so M_W(c, \cdot) = R_{\sharp}\,\mathrm{Law}(z_{\tau}), the pushforward of the stopped-state law along R (equivalently M_W(c, A_Y) = \Pr[R(z_{\tau}) \in A_Y \mid z_0 = (c,\varnothing,m_0)] for a measurable A_Y\subseteq\mathcal{Y}); the no-truncation special case takes \mathcal{Y}=\mathcal{C} with R(c,b,m)=c (the window is the whole transcript), reading c_{\tau} directly. The \bot branch is exactly what \gamma rejects fail-closed. This is a specialization, not part of the definition: a harness wrapped around a black-box API is still a harness, and M_W may be any learned kernel. Where the weights are open, the geometry of \Phi_W is where the substrate's continuity lives, and several downstream claims lean on it — but the definition does not.

Two stopped processes, nested: deterministic control over stochastic dynamics over a learned kernel. Both loops are hitting-time processes; some harnesses additionally read the halt set as a fixpoint or acceptance condition — iterative refinement to self-consistency is the genuine fixpoint case, while EOS, length, and tool-call syntax are not convergence. Neither loop settles because you asked it to. (The clean inner-then-outer nesting assumes tool calls fall between model runs; streaming or mid-generation tool calls interleave the two loops and need a finer state machine — the nesting is then an idealization.)

Reading it

Symbol	Is
\mathcal{H},\ \mu_0	the harness — the whole controlled system, not the model — with initial law \mu_0 on \mathcal{S} a member of the tuple (determinism is conditional on a fixed s_0; a free \mu_0 is itself a coin)
s \in \mathcal{S}	task-state: IR / dialect stack, tool results, plan, counters, and every mutable interface variable (model/tool versions, permissions, retrieved context) — only Markov after that augmentation. Factored where precision demands it (The outer kernel) as s=(q,w): controller-observable q (what \pi,\gamma,\rho read) and possibly-latent world state w (what only Q_E touches); the observed effect o is the receipt Q_E returns, in general reported not actual. Elsewhere the single s means q where a controller map reads it, w where Q_E reads it, (q,w) where reach-avoid is evaluated
\mathcal{C},\ \mathcal{Y},\ \mathcal{A},\ \mathcal{E}	the context / readout / action / effect spaces — model-visible context \mathcal{C}, model readout \mathcal{Y} (incl. the parse-failure \bot_{\mathcal{Y}}, emitted by M_W when no readout forms), authorized actions \mathcal{A} (with \mathcal{A}_{\bot} = \mathcal{A}\cup\{\bot_{\mathcal{A}}\}, the authorization rejection returned by \gamma), and tool/environment effects \mathcal{E}; the two $\bot$s are distinct events — un-parsed vs parsed-and-refused — both forcing the no-op e_0
\pi : \mathcal{S} \to \mathcal{C}	lowering — prompt construction, dialect lowering, effective-program selection (deterministic)
M_W(c, dy)	the model-run kernel (inner solver) — a stopped autoregressive process; \Phi_W is the residual-stream ("manifold") core in the transformer case
Q_E(s, a, de)	the environment/tool kernel on the authorized action a\in\mathcal{A}_{\bot} (with Q_E(s,\bot,\cdot)=\delta_{e_0}, the no-op e_0) — tool effects, API responses, the world (possibly adversarial); factored (The outer kernel) as Q_E(w,a)\rightsquigarrow(w',o) — the environment reads world state and the authorized action, never q
\gamma,\ \rho	the deterministic authorization gate \gamma:\mathcal{S}\times\mathcal{Y}\to\mathcal{A}_{\bot} (untrusted proposal → authorized action or \bot) and the fail-closed verify-and-fold-back \rho:\mathcal{S}\times\mathcal{Y}\times\mathcal{A}_{\bot}\times\mathcal{E}\to\mathcal{S}
H,\ \tau_H	the halt set (absorbing) and the outer halting time — a hitting-time process, not a single pass
H_{\mathrm{ok}},\ B	the accepting halts H_{\mathrm{ok}}\subseteq H — read operationally as H_{\mathrm{acc}}, what the controller declares accepted (all an implementation can test), as against an analysis-only ground-truth success G\subseteq H that need not be computable (H_{\mathrm{acc}}\setminus G is the semantic-adequacy gap: accepted yet wrong) — and the bad set B, unsafe states for reach-avoid (B\cap H_{\mathrm{ok}}=\varnothing), evaluated on the global (q,w), separate from H and possibly entered mid-run before any halt

The structural fact that earns the word controller: \pi, \gamma, \rho, and the halt test are deterministic (and the readout R too, where the transformer specialization is in play), so \mathcal{H} injects no randomness of its own. Every coin is inherited from M_W and Q_E. This split — deterministic code around a stochastic oracle — wears two names. In control-theory terms it is controller vs. plant: the controller is those deterministic maps; the plant is the learned kernel M_W, plant in its exact sense — the element with its own dynamics you steer but do not author. In engineering terms it is shell vs. plant: the shell is the entire deterministic outer harness — the control logic plus the external memory and tools it administers (the files, databases, vector stores below) — of which the controller is just the control-logic slice. So shell : plant :: the part you write : the part you don't; M_W is the only thing on the right, while the environment Q_E is the world the actions meet — a disturbance into the loop, not the plant. (A reader from reinforcement learning or classical control will make the opposite assignment — environment as plant, policy as controller; the inversion is deliberate: in harness engineering the element you are trying to make behave is the model, and the world is what pushes back on the attempt.) This determinism is conditional — on versioned code, configuration, model endpoint, and tool interfaces, and on single-run sequencing: concurrent runs sharing authorization state re-open a gap the per-run object cannot see (taken up under Gate placement in the appendix); any retry, timeout, race, or randomized routing that escapes that conditioning must be modeled explicitly as part of Q_E or the controller, not waved away. The displayed M_W(c) likewise freezes endpoint, version, and sampler; a routing or config change is a state-indexed kernel M_{\kappa(s)} or folds into K_C — the kernel must not silently depend on config the table places in s. More generally, control may itself be stochastic — a controller kernel K_C(s, dc) over routing, sampled retries, ensemble votes, learned routers — of which the deterministic \pi, \gamma, \rho, H are the Dirac special case. That case is the one worth wanting: it localizes every coin to M_W and Q_E and keeps the controller/plant split clean. Where control is genuinely stochastic the split does not break, it widens — fold K_C into the kernel and the certificate quantifies over its randomness too. But the guarantees do not soften uniformly, and the component-to-guarantee map is worth stating because it says exactly what may be learned without loss. A learned \pi — retrieval, reranking, summarization inside the lowering — costs only semantic adequacy, under one factorization: \pi splits into a deterministic never-lower filter — the redaction that keeps credentials and other principals' data out of \mathcal{C} — composed with learned selection, and only the selection may soften, or the confidentiality floor of the invariants note becomes a probability. With the filter Dirac, no-unauthorized-effect is $\gamma$'s property alone. The reach-avoid certificate does not survive automatically, though — softening \pi into a kernel changes the outer transition kernel T, so a certificate proven for the deterministic \pi must be re-established for the new $T$; what the factorization buys is that the possibility of a certificate is preserved (the provenance partition and the confidentiality floor still hold), not the certificate itself. A learned \gamma or \rho costs the thing itself — authorization and ledger bookkeeping are exactly the properties that must stay Dirac. But determinism buys only consistency, not truth: a deterministic \rho guarantees the ledger faithfully records the response it received, not that the response is what the world did — a tool returning a false but well-formed e makes "the ledger is what happened" a claim \rho cannot secure. The honest split is three objects — the actual world transition w\to w', the observed receipt o (what this document has been calling the effect record's payload), and a soundness/attestation assumption relating o to (w,a,w') — and $\rho$'s integrity is conditional on that assumption; absent it, every status \rho writes is "reported," and \mathsf{unknown} is the honest label for an outcome no trusted attestation covers. So the minimal deterministic core is \{\gamma, \rho, H\} plus $\pi$'s never-lower filter: the rest of \pi may soften into a kernel and the harness bends without breaking — fortunate, because every deployed \pi already has learned kernels inside it.

Why this shape

f(x) \;\longrightarrow\; x = f(x;\,W) \;\longrightarrow\; f(x)

Classical software, inverted into latent geometry, then re-wrapped in classical software. The harness re-imposes the determinism the model dissolved: \pi, \gamma, \rho, and the halt test (H) are ordinary designed code — a controller — whose primitive operand happens to be a stochastic oracle. That closure is why a compiler is the right mental model (staged deterministic software ports cleanly) and exactly why the analogy breaks (a compiler's primitive operation was never a coin). The harness is the half you can reason about classically, sitting on top of the half you cannot.

The limit, stated honestly

Raw halting is cheap; correct halting is not. A certificate is a witness: a checkable object — here a Lyapunov/drift function V \ge 0 — that provably satisfies a condition entailing the guarantee, through a standard supermartingale / optional-stopping theorem (the target picks the condition: drift toward H for halting, a barrier for safety, reach-avoid for success). It is not the property, only an object cheap to check and hard to produce. One word then carries two senses, and the seam between them is what this section is about: the proven certificate, a V whose bound actually holds; and the measured surrogate you fall back on when the architecture exhibits none — a candidate \hat V with a sampled slack \delta, a calibrated risk metric, not a certificate until that bound is proven (or held to a high-confidence worst case). The gap between the two is the whole honest-limit argument. A deterministic budget — augment s with a counter k decremented each outer step, halting at k=0 — makes V(s)=k a trivial Lyapunov certificate for halting, so the architecture does not lack a halting guarantee by construction. What it lacks for free is a certificate of correct, safe, successful halting under the learned dynamics. The un-budgeted halting object is still worth stating, since it shows where even the easy guarantee comes from: a certificate would be sufficient for almost-sure halting with bounded expected runtime — a V \ge 0 with

\mathbb{E}[\,V(s_{n+1}) \mid s_n\,] \le V(s_n) - \varepsilon \quad\text{off the halt set}

bounds \mathbb{E}[\tau_H] \le V(s_0)/\varepsilon under the usual integrability and optional-stopping conditions. Nothing in the harness hands you such a V the way a compiler's structure does: a specific compiler analysis gets its V for free where a finite-height lattice is a well-founded descent — termination by construction for that analysis, not for a whole compiler — and the harness has no analogous built-in descent for its model/environment loop.

But the relevant V is not absent — and this is the subtlety the blunt phrasing erased. The minimal certificate exists and is forced: it is the expected halting time itself,

V^\star(s) = \mathbb{E}[\,\tau_H \mid s_0 = s\,],

finite wherever H is reached in finite expected time — the domain \{s : \mathbb{E}_s[\tau_H] < \infty\} — though note this V^\star certifies halting (reaching the terminal set H at all), not correct halting; the stronger object, the expected time to an accepting H_{\mathrm{ok}} \subseteq H, is V^\star_{\mathrm{ok}}, taken up at the second wall below. So the honest claim splits in two: the architecture provides no certificate for free, and the one that exists is — conjecturally, not as a theorem — a functional of W and the environment that does not compress below model scale. The conjecture needs scoping, because the per-step drift splits by coordinate (made precise below) and the shell's contribution is an exact, designed descent of low description complexity by construction — so whatever is incompressible is not the shell's part but the plant's, the contribution M_W supplies. And even there it is conjecture with a live counter-possibility, not foregone hardness: V^\star is a coarse functional — one scalar, an expected hitting time, not the full output law — and coarse functionals of complicated kernels are sometimes cheap (absorbing chains with sparse transition structure have tractable expected hitting times over enormous state spaces). So the honest form is conditional: if the plant's contribution to the drift admits no certificate of description length materially below |W|, then ours is as hard as the dynamics — but that antecedent is the unproven part, and the flat phrasing of an earlier draft ("the dynamics it certifies are the weights") overstated it by treating a coarse hitting-time functional as if it carried the whole distribution. The compiler's certificate is structurally trivial; ours is plausibly as hard as the plant dynamics, though whether useful compressed certificates exist — for the coarse hitting-time functional, or for structured sub-tasks — is open. This is the quantitative form of you can borrow how LLVM is built — not, in general, why it is correct.

So you never compute V^\star. You pick a candidate \hat V and estimate its drift slack

\delta = \sup_{s \notin H}\Big(\mathbb{E}[\,\hat V(s_{1}) \mid s_0 = s\,] - \hat V(s) + \varepsilon\Big).

The status of \delta has to be stated carefully, because it is easy to oversell. If you can establish a high-confidence upper bound on the true worst-case slack and it is \le 0, optional stopping hands you a real, conservative certificate, \mathbb{E}[\tau_H] \le \hat V(s_0)/\varepsilon. But an empirical \delta estimated from sampled states is not a certificate: a measured \delta > 0 may mean the candidate \hat V is poor, the sampled distribution missed rare failures, the supremum was never attained in-sample, the process is non-stationary, or the state abstraction is not Markov. So \delta is the number on the dashboard — a calibrated risk metric, the evaluable surrogate for a guarantee the geometry will not give you, and a genuine bound only once it is statistically controlled against rare-event and adversarial tests. A weaker result is still useful: a true bound \delta \le \bar\delta < \varepsilon (rather than \le 0) leaves descent intact with effective slack \varepsilon - \bar\delta and \mathbb{E}_s[\tau_H] \le \hat V(s)/(\varepsilon - \bar\delta). And the empirical quantity is distributional, not a supremum — write \delta_{\nu} for drift averaged over a sampled \nu, reserving \delta_{\sup} for the worst-case bound; only \delta_{\sup} certifies. Its empirical noise floor and residual risk are driven by the measure \mu(D) of the divergent region D=\{s:\mathbb{E}_s[\tau_H]=\infty\} (states from which H is not reached in finite expected time, under the reference/sampling measure \mu), the coverage of the sampled state distribution, and the hitting-time variance \mathrm{Var}[\tau_H] — properties of the trained weights, the environment, and the evaluation distribution, knowable only a posteriori.

For an agent meant to run forever — a coordinator, a daemon — halting is the wrong target, and V^\star = \infty is the spec, not a pathology. The same drift theory then certifies recurrence to a ready-state instead of absorption to a halt-set. The object changes; the missing certificate does not. Safety changes shape too: it is no longer the one-shot \Pr_s(\tau_B=\infty) but a per-cycle hazard that compounds — if each ready-state-to-ready-state cycle touches B with probability q, survival over N cycles is \approx (1-q)^N, so a reassuring per-cycle 0.9999 is \approx 0.37 over ten thousand cycles. The reach-avoid certificate for a daemon is therefore a bound on q against the intended horizon — the safety twin of the regenerative expected time that replaces V^\star_{\mathrm{ok}} for restarting specs.

And the consolation rests in part on an assumption the world violates — though less of it than it first seems. The supermartingale bound itself survives a nonstationary kernel, provided the conditional drift holds uniformly at every step; what genuinely needs a time-homogeneous kernel is V^\star as a fixed function, the resolvent / fundamental-matrix identities, and the sampled-\delta calibration (which assumes the very kernel it was measured on). But the environment E is part of T, and the world is not stationary — worse, it can be adversarial, an attacker choosing the tool-output policy — a kernel over what tools return, not the realized draw — so as to break your descent. The drift condition then stops being a fixpoint question and becomes a minimax one,

\sup_{\alpha \in \Pi}\ \int_{\mathcal{Y}}\!\int_{\mathcal{E}} V\big(\rho(s, y, \gamma(s,y), e)\big)\, Q_E^{\alpha(s,y)}\big(s, \gamma(s,y), de\big)\; M_W(\pi(s), dy) \;\le\; V(s) - \varepsilon,

a descent that must hold in expectation over the model's own output y and even when the adversary picks the worst admissible environment policy \alpha(s,y) from the class \Pi of policies the environment genuinely permits — every \alpha\in\Pi must still respect rejection, \gamma(s,y)=\bot \Rightarrow Q_E^{\alpha}(s,\bot,\cdot)=\delta_{e_0}, or the adversary resurrects side effects the gate refused. Well-posedness is a frontier caveat of its own: for \sup_{\alpha\in\Pi} to be attained rather than merely defined, \Pi needs structure — measurability of \alpha\mapsto Q_E^{\alpha}, compactness of the per-state admissible set, or a measurable-selection theorem furnishing a worst-case \alpha — and "respects rejection" is a constraint on \Pi, not that existence argument; on a general state space the sup may have no maximizer, in which case the certificate quantifies over a maximizing sequence rather than a single adversary. A V that certifies halting against a benign world is defeated by an adversarial one, and the measured \delta bounds only the Q_E you sampled, never the policy an attacker will choose. One note on the adversary's information: writing \alpha(s,y) lets the policy condition on the raw readout y, which the real environment never sees — it sees only the authorized action a=\gamma(s,y). This is deliberate, and it is the conservative direction: an adversary given the stronger oracle (the pre-gate proposal, not just the post-gate action) can only make the worst case worse, so a certificate that survives \sup_{\alpha} over \alpha(s,y) survives the implementation's true adversary class \alpha(w,a) a fortiori. Where the gap matters — an over-approximation is looser than the real threat model — the honest form restricts to \alpha(w,a); the document quantifies over the stronger \alpha(s,y) except where noted.

This is the formal home of prompt injection — not "the model did something bad," but the environment optimized to bend your dynamics. And the target is not merely non-halting: injection steers toward a bad set B — wrong acceptance, data exfiltration, unauthorized tool use, privilege escalation, irreversible side effects — so security is a reach-avoid problem, not a liveness one.

Here two reliability objects must be kept apart, because under absorbing refusal every naive intermediate collapses into one of them:

p_{\mathrm{succ}}(s) = \Pr_s\big(\tau_{H_{\mathrm{ok}}} < \tau_F\big), \quad F = B \cup (H \setminus H_{\mathrm{ok}}), \qquad\qquad p_{\mathrm{safe}}(s) = \Pr_s\big(\tau_B = \infty\big).

Success is reaching a correct halt before any failure — a safe refusal counts against it. Safety is never entering the bad set at all — a safe refusal satisfies it. These genuinely differ on any run that avoids B without reaching H_{\mathrm{ok}} (p_{\mathrm{succ}} scores 0, p_{\mathrm{safe}} scores 1): safe refusals, and — absent almost-sure absorption into H\cup B — safe non-halting or endless safe retry. The tempting middle form \Pr_s(\tau_{H_{\mathrm{ok}}} < \tau_B) is not a third object, by a two-line case analysis: for it to differ from p_{\mathrm{succ}}, a run would need \tau_F < \tau_{H_{\mathrm{ok}}} < \tau_B — a non-accepting terminal hit strictly before success, then success anyway — which forces exiting H \setminus H_{\mathrm{ok}}, impossible while H is absorbing. Note what does not re-separate them: within-run fail-closed retries (the non-terminal fail-closed of the definition) never touch F at all — the rejected proposal lands in a safe non-terminal state — so a refuse-retry-succeed run scores 1 on both forms, and the coincidence survives any amount of retrying. The middle form becomes a genuine third object only when the two hitting times can genuinely part ways: under restarting specs, where an owner re-launches out of a refusal terminal and the absorbency of H \setminus H_{\mathrm{ok}} is deliberately dropped (the regenerative reading the daemon note above already contemplates) — no bookkeeping needed, since hitting times record visits, not occupancy, so the relaunched run's \tau_F is already finite — or under a failure set that counts refusal events accumulated in s, F' = B \cup (H \setminus H_{\mathrm{ok}}) \cup \{\mathsf{refusals} \ge 1\}, which separates the forms even within a single run. In the restart case a run may halt refused, restart, and still reach H_{\mathrm{ok}} before B: the middle form credits it; p_{\mathrm{succ}}, measured against the refusal it passed through, does not. Safety is certified by a barrier / avoidance certificate for B; success needs that plus the reach part — a hitting-time drift toward H_{\mathrm{ok}}. Fail-closed control is the disturbance-rejection margin for both, but split by reversibility: the gate \gamma caps how far an adversarial world reaches into side effects and widens the gap to B (it is the margin for the irreversible part), while \rho validates the response and folds back, rejecting bad state after the action has run — which cannot undo an authorized side effect. In this language, security is robustness of the reach-avoid certificate.

And injection is not confined to the post-model kernel Q_E: poisoned retrieval, prompt-injected pages, and malicious tool metadata enter through $\pi$'s inputs, before generation — so the adversary lives wherever untrusted content enters the state/context-construction pipeline, which is why input provenance and the gate \gamma both matter, not post-hoc verification alone. And provenance is a precondition of the certificate, not just an entry point to police: partition s into a control-determining part — plan, intent, what is authorized next, the coordinates \pi lowers and \gamma checks — and a data part — tool values, retrieved text, the bytes of e. Reach-avoid presupposes untrusted effects touch only the latter; let \rho fold attacker-controlled e into the control part and the structural-intent check validates against a plan the adversary already bent, collapsing \gamma to the strength of $\rho$'s validation. So the claim is conditional — reach-avoid given control flow provenance-isolated from untrusted data, the isolation that makes provable security possible (the content of CaMeL's control/data-flow separation, untrusted data filling typed values but never the program), a structural property the harness supplies and \rho cannot recover after the fact. And "provenance" is really two labels that propagate in opposite directions, which a single lattice conflates: confidentiality (a secret must not be lowered into \mathcal{C} — combined conservatively upward, a value is as secret as its most-secret input) and integrity (untrusted content must not reach authority — combined downward, a value is as trusted as its least-trusted input). The control-determining partition here is the integrity axis; the never-lower filter of the component map is the confidentiality axis; a full label is the pair, and declassification (lowering confidentiality) and endorsement (raising integrity) are explicit trusted operations, never side effects of a transformation. The partition then forces a question the isolation rule alone cannot answer: something must be permitted to write the control-determining part mid-run — or no plan could be steered, no approval granted, no scope widened — and naming that something is part of the object. It is the trusted principal: the owner of the run. An approval request is an ordinary authorized action through \gamma into Q_E — ask-the-owner is a tool call to the one counterparty you trust — and its response is the single class of e that \rho may fold into control coordinates; every other e folds into data. This is not an exception eroding the partition but the partition completed: a provenance lattice with a top the model cannot reach, which is what trusted means. "Exactly one writer" is the simplest such top and the profile this document develops, but it is a deployment choice, not a formal necessity — threshold approvals ($k$-of-n), multiple authenticated principals with disjoint scopes, and quorum endorsement are legitimate tops too (top read as the model-unreachable upper region — in the disjoint-scope case an antichain of maximal writers, not one element), all sharing the one property that matters: the widening authority is not a learned kernel — and the appendix's gate-placement entry derives the matching rule for learned verdicts, which may never stand in this writer's stead. One distinction keeps the lattice from outlawing the loop it governs. Control-determining is not one rank but two: authority — grants, scopes, budgets, what the principal has permitted — which only the top writer widens; and the plan, which the model rewrites at every fold of y, because replanning is the harness. The plan is a middle rank: written through the gated fold of the model's own output — the channel the minimax descent above already prices — never directly by an effect, and never a source of widened authority. The rank is also the field's live design axis: pin plan-writes to the top-derived rank — the plan fixed from the trusted query before any untrusted read, which is CaMeL's move — and provable security follows exactly there; let the middle rank replan interactively and you pay the adversarial price the certificate quantifies. A corollary with teeth: a dedicated planning component is rank-neutral — its writes land in the same middle rank as the model replanning inline — so it changes no guarantee and lives or dies on measured capability alone; in general, sub-components that only write middle-rank state are priced by evals, not by the certificate, which prices only rank crossings, gates, and \Pi. (For B to capture irreversible side effects rather than only states, the side-effect ledger must itself live in \mathcal{S}, and the response e must be an effect record carrying the ledger outcome — not just API bytes — since only \rho writes external effects into s.)

There is a second wall, orthogonal to the first. It binds not the full harness state \mathcal{S} but the model-visible working memory \mathcal{C} = \mathcal{V}^{\le L} — bounded by the context length L. That bound is not the incompressibility of V^\star (a fact about the parameters W — the dictionary, fixed at training); it is a fact about the inner kernel's working memory (the L\times d residual stream — the desk). \mathcal{S} itself may be far richer — files, databases, vector stores, durable memory, queues — but that is external memory the shell supplies, and the distinction is the point: every external read still passes through the \le L window to touch computation, so external stores extend addressable storage without extending the per-pass resident set. The shell can page; the plant cannot grow its desk. (What follows is heuristic, not definition-level: the complexity claims turn on depth, precision, and architecture, and belong with the frontier, not the core.) The tape picture comes from the autoregressive structure alone and needs no complexity theorem: each step reads a bounded window and writes one token, so the context window is the tape, the autoregressive loop is the read/write head, and — in the variable-L, fixed-precision idealization — the model-mediated inner computation behaves like a linear-bounded automaton, its reachable fixpoints capped by space-O(L) computability (chain-of-thought is register-spilling onto that tape). Separately, and more weakly, there is a per-pass expressivity bound: under the standard fixed-depth, log-precision theoretical model a single forward pass is in constant-depth \mathsf{TC}^0 — suggestive for deployed models, not literal (real models use fixed-point precision and depth that grows with scale, and log-depth variants escape parts of it). These are different resources — the first bounds the space the loop addresses, the second the depth of one step — and only the space bound carries the $L$-wall; chaining them (one pass buys bounded depth, therefore the loop is space-O(L)) would be a non-sequitur, since per-step depth says nothing about the length of the tape the loop runs on. This is a second obstruction beside divergence, and it concerns success, not raw halting. Split the terminal set: let H be any halt state (including fail-closed refusal) and H_{\mathrm{ok}} \subseteq H the successful, accepting halts, with V^\star_{\mathrm{ok}}(s) = \mathbb{E}[\tau_{H_{\mathrm{ok}}} \mid s_0 = s] taken on the process where H \setminus H_{\mathrm{ok}} — halting wrong, refusing, failing closed — is absorbing failure, so a run that fails closed before acceptance has infinite accepting hitting time unless the spec explicitly restarts it — hence unconditional V^\star_{\mathrm{ok}} is infinite whenever pre-acceptance failure has positive probability, which is why the workable reliability object is the success probability p_{\mathrm{succ}} (above) or, for restarting specs, the regenerative expected time. Then U_{\mathcal{H}}(L) — harness-relative, since the shell's decompositions and verified tools determine what can be paged or outsourced — is the set of tasks whose irreducible per-step model-mediated working set exceeds L — not tasks whose data exceeds L (those the shell can page), and not work that can be discharged to a verified external tool (a solver, interpreter, or compiler computes off-context). For a task in U_{\mathcal{H}}(L) the raw chain may still hit H — by failing closed, refusing, or returning a wrong answer — so V^\star = \mathbb{E}[\tau_H \mid s] stays perfectly well-defined; what blows up is V^\star_{\mathrm{ok}}, the expected time to a correct halt, which is infinite under a formal success predicate, or undefined if no such predicate has been specified. The honest statement is about the finite-success domain, and it is schematic — a shape written in set notation, not a theorem, since \mathrm{reachable}_{\mathcal{H}}(L) is exactly as informal as the working-set notion behind U_{\mathcal{H}}(L): \mathrm{dom}_{<\infty}(V^\star_{\mathrm{ok}}) \subseteq \mathrm{reachable}_{\mathcal{H}}(L) \setminus D — both the reachable set and the divergent set D relative to \mathcal{H}. The two walls trade — directionally, not as a literal exchange rate: parametric memory |W| and working memory L press on the same budget along the pretraining-vs-inference-scaling axis, with no clean unit-for-unit substitution of one for the other. And the bound is inherent to finite working memory, not attention specifically: state-space models embody it differently (a fixed-size recurrent state rather than an $L$-window), and real attention's usable tape is shorter than L (lost-in-the-middle).

Where it cashes out

This is not ornament; the decomposition is load-bearing in the design.

• \pi is a progressively-lowered dialect stack — raw input → intent → plan → tool-call → the neutral wire IR — each level a deterministic pass with its own verifier — pass and verifier meaning the shell's transformation and checking: the content entering at the plan level is plant-authored, middle-rank state (the two-rank note of The limit), which is exactly why that level carries a verifier at all. The per-step drift r(s)=\mathbb{E}[\hat V(s_{n+1})\mid s]-\hat V(s) splits by coordinate, r = r_{\text{shell}} + r_{\text{plant}} + r_{\text{env}} — presuming an additively separable \hat V, or a declared scheme attributing each step's drift to shell, plant, and environment coordinates: the shell term is an exact, designed descent — but per lowering pass, not per outer step: each pass strictly narrows the admissible-meaning set, a well-founded descent we build by hand, while the outer loop revisits — retry, replan, rewind are planned ascents of any reasonable \hat V, which the run-level certificate must absorb (a retry budget inside \hat V is the standard device), so the shell's descent is well-founded in the nested, lexicographic sense rather than monotone along the run; the plant term (M_W) is the irreducible residue, and the environment term (Q_E) is the one an adversary controls — the very quantity the minimax descent must bound, which the old two-way split folded out of sight. Syntactic soundness is free; semantic adequacy is not. Relative to a formal schema and a correct validator, schemas, types, and boundary checks go into the shell at zero probabilistic cost; whether the lowered task still means what the user intended stays empirical, because natural language supplies no source-language standard to check against.
• \rho is fail-closed verification — validate at every boundary, never let malformed state flow downstream. The discipline transfers from compilers in form; the teeth do not, because a harness has no source-language standard — natural language is, in effect, all undefined behavior — there is no complete formal source-language semantics to check against. And \rho must be deterministic: if verification is itself an LLM judge, that is another learned kernel call — it belongs in M_W, not in \rho. Where \rho repairs rather than rejects — canonicalizing malformed input into valid shape — remember that repair is an authorization decision in disguise: each repair rule converts a reject into an accept on bytes the adversary chose, so it must be deterministic, meaning-narrowing, and its output re-validated as if it had arrived that way, or the repair pass is a bypass of the very boundary it serves.
• \delta, \mu(D), \mathrm{Var}[\tau_H] are what you measure — not derive. You instrument the certificate precisely because the architecture does not hand it to you — you estimate it unless it is separately certified. And the meter is attack surface: if \hat V is itself computed by a learned judge — a model scoring "progress" — the instrument is a kernel draw with the plant's own adversarial exposure, and an environment optimized to bend your dynamics will bend your measurement of them first; an injected page persuading the judge that work is advancing is precisely a divergence hidden from the dashboard built to catch it. The rule that put the LLM judge in M_W, not \rho, applies to instrumentation too: a learned \hat V is part of the measured system, never a neutral meter.

How this could be wrong

It is a hypothesis; here is what would falsify it. If the controller cannot in practice be kept deterministic — if real reliability demands stochastic control the plant can't absorb — the clean deterministic split is a fiction (the broader K_C kernel model still holds, but loses its payoff: localizing every coin to the plant). If the drift slack \delta turns out not to track real-world failure, the whole "measure the certificate you can't prove" program is empty. And if harnesses are simply better described some other way — not as nested stopped chains at all — then this is a pretty equation that merely happens to fit, an elegance we would be right to distrust.

First, handles — the load-bearing claims numbered, so the tests have addresses. C1: the harness is faithfully modeled as nested stopped Markov processes — the tuple, the outer T, the inner M_W — and the implementation realizes the normal form, with no channel the diagram omits (the realizability clause of the invariants). C2: the controller injects no randomness — given a fixed s_0, every coin localizes to M_W and Q_E. C3: fail-closed is a gate property on the realized contract — no effect crosses unvalidated (the environment reading Q_E(w,a), not full s), rejection is a true no-op, and the safe set K is closed under it. C4: no certificate of correct halting comes free, and the measured slack \delta is a calibrated risk metric, never a certificate. C5 (conjecture): the minimal certificate of correct halting against the plant admits no representation materially below model scale — scoped, because it is easy to misstate. It is not a claim that no compact super-solution of the bare-halting drift exists — slack there is cheap: the budget certificate V=k has non-positive slack for \tau_H by construction; it is a claim about the description length of any object whose worst-case slack is non-positive for the correct-halting drift — descent toward H_{\mathrm{ok}}, not merely toward H — in a fixed representation language at fixed precision and tolerance over a stated task domain. Absent that quadruple — language, precision, tolerance, domain — "below $|W|$" is not yet well-defined, and pinning it is part of what C5 owes. C6: two orthogonal walls — divergence (\mu(D)) and the $L$-bounded per-pass working set. C7: security is reach-avoid, certifiable only conditional on integrity-provenance isolation with a trusted top (B evaluated on global (q,w), and H_{\mathrm{cancel,unresolved}} counted as possibly-bad) — the certificate holding relative to the attestation assumption relating reports to actual effects. C8 (figure): certificate and interlingua are one object — already demoted by its own section, and exempt below accordingly.

Each claim is operational, not merely rhetorical:

• State-ablation (C1 — the Markov claim). Drop a variable from s and check whether next-step transition statistics move. If they do, the abstraction was not Markov, and s must be augmented until it is. (Passing is necessary, not sufficient — the test can falsify Markovity, not establish it.) The same probe pointed at \pi tests lowering sufficiency: drop a coordinate from c rather than s and watch task success rather than transition statistics — context compaction lives or dies by exactly this.
• Controller-determinism audit (C2). Re-run with model samples and tool outputs held fixed. Any residual variance is randomness the harness itself injected — clock reads are the classic leak (timestamps folded into s, wall-clock timeouts, cache expiries) — and must be folded into Q_E or the controller, or the determinism claim is false.
• Drift calibration (C4). Test whether $\hat V$-drift actually predicts failure, retry count, latency, or non-halting. One uncorrelated candidate kills that candidate, not the program; the program is empty only if candidates from the natural families — plan depth, open-obligation counts, budget burn, judge scores — systematically fail to track failure.
• Adversarial-environment test (C7). Replace sampled E with worst-case tool outputs, prompt-injected documents, poisoned tool metadata, malformed responses. The minimax descent must survive these, not merely the benign draw.
• Boundary-control ablation (C3, C7). Compare prompt-only defenses against deterministic tool-call validation, capability checks, sandboxing, and fail-closed rejection at the gate \gamma. The hypothesis predicts the latter class dominates; if prompt-only defenses match it, the controller/plant security story is wrong.
• Readout-typing check (C1, C3). Verify that $M_W$'s codomain is exactly what \gamma consumes — especially under window truncation, where the final context need not hold the full transcript, so the output buffer and the gate's input must still agree.
• Certificate-compression search (C5). The conjecture falsifies constructively: exhibit a \hat V of description length far below |W| whose worst-case slack for the correct-halting drift — toward H_{\mathrm{ok}}, C5's quadruple fixed — is provably \le 0 over a nontrivial task domain. The text concedes the live counter-possibility — coarse hitting-time functionals of complicated kernels are sometimes cheap — so C5 stands only until someone cashes it.
• Working-set probe (C6). Fix the shell and scale a task family's irreducible per-step working set past L, on tasks the shell can neither page nor discharge to a verified tool — anchoring "irreducible" in families with proven streaming or communication-complexity lower bounds, so the floor is someone else's theorem and a solved family cannot retreat to reducible-after-all. State it as a success-probability ceiling, not a cliff: a space bound caps achievable accuracy, so the falsifiable form is \sup_{\mathcal{H}\in\mathfrak{H}_L} p_{\mathrm{succ}}(\mathcal{H},\mathcal{D}_n)\le 1-\eta — success scored against the family's ground truth G, never the harness's own H_{\mathrm{acc}} (a rubber stamp beats any self-scored ceiling vacuously), \mathcal{D}_n the family at working-set scale n, and the bound holding for some \eta>0 uniform in n past L — over a precisely defined resource-bounded harness class \mathfrak{H}_L (fixed L, bounded parser state and readout, fixed precision) — not an abrupt collapse and not an infinite V^\star_{\mathrm{ok}}. A family in \mathfrak{H}_L solved reliably past the bound, without new shell decompositions, falsifies the wall.

Where this points (the frontier — least falsifiable, so flagged)

If V^\star is incompressible only in token coordinates, the right change of coordinates might compress it — and that change of coordinates is a representation of meaning itself. Cost-to-go and representation co-determine each other: where the Koopman operator is diagonalizable — a point-spectrum idealization, since mixing dynamics carry continuous spectrum and admit no eigenbasis — the eigenbasis that linearizes the dynamics is also the one in which the certificate decomposes, and even then only for a V in the span of those eigenfunctions; in reinforcement learning the discounted successor representation (Dayan 1993) is the resolvent (I-\beta P)^{-1} — discount \beta, not the gate \gamma — with V a linear readout of it — and in the undiscounted, absorbing case that actually matches a stopped harness the same role is played, in the finite setting — and countable settings where the Neumann series converges — by the fundamental matrix N = \sum_{n \ge 0} Q_{\mathrm{tr}}^{\,n} (written (I - Q_{\mathrm{tr}})^{-1} when the inverse exists), where Q_{\mathrm{tr}} is the sub-stochastic kernel restricted to H^c (transitions before absorption at H) and the row sums N\mathbf{1} are V^\star on the finite-mean hitting domain; on general state spaces the same series is read as the potential (Green) operator G, with G\mathbf{1} = V^\star wherever it converges. Each of these is a clean identity only for a fixed, time-homogeneous kernel — under a nonstationary Q_{E,n} the resolvent and fundamental matrix dissolve into a time-ordered product, and under an adaptive adversary into a controlled / game-value operator, so what is identity in the stationary regime is analogy beyond it.

With that caveat, the interlingua and the certificate are one object seen twice — and the reason neither can be written in closed form is the same "all undefined behavior": no canonical lowering of meaning, hence no finite header-file for either. The only representation of both is W — a band-limited, lossy compression of a scale-free meaning-space, sharp where the record is thick and blurred where it thinned. That a finite object renders an infinite one lossily but honestly — declaring its resolution, and where it is unsure — is not a lie; it is the most an f(\cdot\,;W) can do. The search for V and the search for the interlingua are not two programs. They are one — and the day either is written in closed form, so is the other, or we will have proven why neither can be. Read this as figure, not a lurking theorem: the only precise version would need the Koopman eigenbasis to fall on the very coordinates that lower meaning, and the mixing-spectrum caveat above already concedes that eigenbasis does not exist — which guts it. It is the least-defensible claim in this document, and it should announce that rather than imply a rigor it has not got.

The loop

This section opens an object rather than settling it; it is a sketch of where the same construction goes one level out, flagged as unfinished.

Everything above governs a run: a principal poses a task, the harness drives it to a halt, the principal reads the result. Step back once and there is a further loop that this document has treated as exogenous — the process that decides what the next task is, dispatches it, checks the result, remembers, and fires again. In one recent framing this is the difference between the harness (the scaffold the run executes in) and the loop (the recurring trigger–act–verify–stop cycle that keeps launching runs); the practitioner literature that named the loop treats it as a layer above the harness. The claim worth making here is that this is not a new kind of object at all — it is the harness construction applied one level out, with a run where a step used to be.

Make the correspondence exact and the reuse is total. The outer loop has its own state s^{\uparrow} (a backlog, a set of open goals, what has been tried and what passed), its own lowering \pi^{\uparrow} (which goal to pursue now, and with what context), its own plant — but the outer plant's proposals are whole runs, so the inner harness plays the role of the outer environment kernel: dispatching a task is one draw of Q_E^{\uparrow}, and the run's terminal ledger is the effect record folded back by \rho^{\uparrow}. This is precisely the composition correspondence of the appendix read at the top level — a child harness is a Q_E component — which is why the loop needs no primitive the tree did not already have. One typing caveat carries over from the atomic-step refinement: a child is a single Q_E draw only when it is non-interruptible from the parent's view — dispatched, then awaited to a terminal ledger. An interruptible child that emits intermediate effects the parent can observe or cancel mid-run is not one draw but a semi-Markov excursion (an options / product-process semantics), the same phase expansion the resume entry forces, one level up. The daemon entry is the special case where the outer loop is a single long-lived agent recurring to a ready set; the general loop is a daemon whose excursions are themselves full harness runs, which is to say the outer-outer harness is a daemon over runs, and inherits that entry's whole ledger: renewal-reward rates, the accumulation that breaks regeneration, hygiene as renewal structure, authority frozen between owner contacts.

What the level shift buys is that the invariants reappear with sharper teeth, because the outer plant is now itself an agent, not a token-sampler. The gate is still the load-bearing object: who authorizes a run? A loop that launches tasks against production is choosing actions with effects, and "the loop decided to refactor the auth module" is an authorized action or an ungated one — the trusted-principal lattice does not dissolve at the outer level, it recurses, and the autonomy corollary bites hardest here, since a loop whose principal has stepped away is exactly the "replace yourself as the prompter" regime, running on frozen authority against a moving world. The two walls recur too: the outer working set is the backlog the loop can actually hold coherent at once (context, one level up), and the outer certificate is the same absent object — no free proof that an unattended loop halts, converges, or stays out of B over a long horizon, only the measured drift of its progress meter, carrying the same warning that a learned outer meter is attack surface. And the degenerate case is instructive in the document's own terms: the brute "same prompt in a while-loop until the spec passes" that the practitioner literature cites as the origin pattern is the outer harness with \pi^{\uparrow} constant, \gamma^{\uparrow} trivial, and verification outsourced to whatever the tests happen to check — the trivial-group harness of the signature-vs-strength note, one level up. It satisfies the outer signature and earns almost none of the outer guarantees, which is exactly why it works until it doesn't.

What this section does not yet do: give the outer objects the same treatment the inner ones got — the precise outer analogue of fail-closed when the "action" is a whole run with partial effects, the right reach-avoid formulation when the bad set is a property of a trajectory of runs rather than one run, the outer verifier's own soundness, and whether the recursion terminates upward or is genuinely open (loops that launch loops). Those are the next rounds. The point of opening it now is only the structural claim: the layers the practitioner stack separates — words, context, harness, loop — are, formally, one object at four scales, and the guarantees this document is about live in the closure at every scale, never in any single layer alone.

---

The formula is the architecture; the corollary is why the architecture is hard. Both on the page — nothing hidden behind a tidy composition.

Grounding

Borrowed theorems are real; the framings are not — keep them separate. Some framings are nonetheless corroborated — independently reached from another field — a third grade, weaker than proof and noted last.

Proven (citable). Foster–Lyapunov drift ⇒ positive recurrence + \mathbb{E}[\tau]\le V(s_0)/\varepsilon (Foster 1953; Meyn & Tweedie, Markov Chains and Stochastic Stability, 1993) — positive recurrence needs the usual irreducibility/petite-set hypotheses, while the absorbing-halt case used here needs only the weaker supermartingale optional-stopping hitting-time bound. The minimal V is the expected hitting time, by first-step analysis + optional stopping (Norris, Markov Chains, 1997). For an absorbing chain that expected hitting time is the row sum of the fundamental matrix N=\sum_{n\ge0}Q_{\mathrm{tr}}^{\,n} (Kemeny & Snell, Finite Markov Chains, 1960), with the general-state analogue the potential (Green) operator (Revuz, Markov Chains, 1984). Koopman's linear-operator view of nonlinear dynamics is classical (Koopman 1931), and Lyapunov functions can be assembled from its eigenfunctions when the spectrum is suitable (Mauroy & Mezić, 2016). You certify a candidate \hat V by a proven drift inequality rather than by deriving V^\star, and estimate it empirically only where a proof is out of reach — the empirical drift checks, it does not certify (neural-Lyapunov: Chang, Roohi & Gao, Neural Lyapunov Control, NeurIPS 2019, arXiv:2005.00611). A classical monotone data-flow analysis gets its V for free because a finite-height lattice is a well-founded descent (Kildall, POPL 1973). The gate-a-plant architecture itself is classical: supervisory control theory synthesizes a deterministic supervisor that disables controllable events of a plant it does not author, with the supremal controllable sublanguage as the largest admissible behavior (Ramadge & Wonham, SIAM J. Control and Optimization, 1987) — \gamma is that supervisor, with a learned stochastic plant on general state spaces; the same theory's controllability condition (specifications must be closed under uncontrollable events) and its nonblocking requirement are the proven ancestors of gate-early-on-irreversibles and of the always-enabled escape the appendix requires behind any learned veto. Covert-channel discipline — identify the channel, measure its bandwidth in bits, audit what cannot be closed — is the TCSEC lineage (A Guide to Understanding Covert Channel Analysis of Trusted Systems, NCSC-TG-030, 1993). The successor representation is Dayan (Improving Generalization for Temporal Difference Learning: The Successor Representation, Neural Computation 1993). Dialect-stack architecture: MLIR (Lattner et al., CGO 2021, arXiv:2002.11054); learned pass-ordering: MLGO (Trofin et al., arXiv:2101.04808). Single-pass low-depth expressivity: log-precision transformers are simulable by constant-depth logspace-uniform threshold circuits (\mathsf{TC}^0) (Merrill & Sabharwal, The Parallelism Tradeoff: Limitations of Log-Precision Transformers, TACL 2023) — fixed/constant precision is a stronger restriction, added autoregressive steps escape it (Merrill & Sabharwal, The Expressive Power of Transformers with Chain of Thought, ICLR 2024), and growing precision changes the picture, so the bound is suggestive for deployed models, not literal.

Asserted (ours — not theorems). That the harness is best modeled as nested stopped chains; that V^\star is incompressible (no compression theorem); that "no lattice for $f(\cdot,;W)$" means none is known, not that none exists; and everything under Where this points and The loop — including the Koopman/certificate co-determination, which is well-posed only under the spectral assumptions noted there, and the interlingua/certificate identification; and the design rules read off the objects rather than proven from them — the single-trusted-writer completion of the provenance partition (a deployment profile, not a necessity — threshold and multi-principal tops are admissible), the narrow-only rule for learned checks and its influence-side twin (verdict payloads to the plant selected, never generated), the composition law of the appendix, and the reading of the tuple as a causal normal form whose guarantees are properties of a realizing implementation relative to a stated attestation assumption, not of the signature. These organize the design; they are not results.

Converged-upon (independently arrived at, from other framings). The Asserted claims above are ours but not ours alone; several are reached independently, from starting points unconnected to this framing — which is the corroboration a definition earns: not a chorus of agreement (the systems below often disagree on method and goal), but that work approaching from capabilities, reinforcement learning, control theory, software architecture, and language-modeling theory each lands on a piece of the same object. That the deterministic controller, not the model, carries the guarantee is reached from four directions — capability and information-flow control (CaMeL: Debenedetti et al., Defeating Prompt Injections by Design, arXiv:2503.18813, securing the agent even when the underlying model is susceptible); reinforcement learning (shielding: Alshiekh et al., Safe Reinforcement Learning via Shielding, AAAI 2018, arXiv:1708.08611 — a deterministic reactive shield filtering a learned policy's actions against a temporal-logic specification); control theory (Stable Agentic Control, arXiv:2605.03034, enforcing finite action catalogs at the tool-output interface under a Lyapunov input-to-state-stability certificate against adversarial disturbance); and software architecture (the plan-then-execute / control-flow-integrity line, e.g. Beurer-Kellner et al., Design Patterns for Securing LLM Agents against Prompt Injections, arXiv:2506.08837). The certified-vs-measured split is reached from the construction side (CaMeL's provable security) and, independently, from the destruction side (guardrail-evasion results — Bypassing Prompt Injection and Jailbreak Detection in LLM Guardrails, arXiv:2504.11168, the v1 title — later versions retitle it; No Free Lunch with Guardrails, arXiv:2504.00441), with verification-oriented work stating it as the motivating gap (Towards Verifiably Safe Tool Use for LLM Agents, arXiv:2601.08012; VeriGuard, arXiv:2510.05156): a learned safeguard raises the odds of detection but cannot guarantee safety against a persistent attacker. The inner readout as a composition of Markov kernels is independently formalized in language-modeling theory — the autoregressive step as kernel composition in the category \mathsf{Stoch} (A Markov Categorical Framework for Language Modeling, arXiv:2507.19247), and the broader "LLMs as Markov chains" line — though that work models the inner kernel alone and never closes it into an agentic loop, which is exactly the seam this definition adds. That provenance shrinks the admissible adversary is reached by datamarking / spotlighting (Hines et al., arXiv:2403.14720, 2024) and by CaMeL's data/control-flow separation; and a systematization of prompt injection against agentic coding assistants reaches the same verdict from the attack side — mitigation must be architectural, not model-level (Prompt Injection Attacks on Agentic Coding Assistants, arXiv:2601.17548); the sharper open problem this object is built to answer — formally specify the trust boundaries, then verify implementations respect them — is our phrasing of where that verdict points, not the paper's. Two convergences are weaker, and flagged. The reach-avoid hitting-time certificate is the independently developed reach-avoid supermartingale (RASM, arXiv:2210.05308, AAAI 2023) and stochastic Lyapunov–barrier apparatus, and its hardness is corroborated — expected-stopping-time problems for Markov chains are inter-reducible with the Positivity problem, a relative of the Skolem problem (Chatterjee & Doyen, Stochastic Processes with Expected Stopping Time, arXiv:2104.07278) — but this supports generic hardness only, not the specific incompressibility-at-|W| conjecture, which remains ours and unproven. And injection as an adversarial policy is corroborated as a minimax game in the detection setting (DataSentinel: Liu et al., A Game-Theoretic Detection of Prompt Injection Attacks, arXiv:2504.11358) and as adversarial-disturbance robustness (Stable Agentic Control, above) — but no prior work assembles it as reach-avoid over the tool-output kernel with the gate as the irreversibility margin; here the relation is adjacency, not convergence.

---

Appendix: model implementation

The definition is deliberately abstract: \pi, \gamma, Q_E, \rho are roles, not code, and a deployed harness forces concerns the abstract object is silent on. This appendix does not re-derive the implementation; it establishes a pattern — take a hard practical concern, locate it in the objects already defined, and read off the discipline they imply rather than inventing new machinery. Cancellation is the worked example, chosen because it is where the silence bites hardest and because the answer falls entirely out of objects already on the page.

Cancellation. An owner stops a running agent mid-flight — worst across a task-agent tree. The naive reading is "stop and undo," but the irreversibility point forbids it: \gamma is the last line before irreversible effects, and \rho can reject a response but cannot undo an authorized action. So cancellation is not making it not have happened; it is a disciplined stop with a defined disposition for what is already irreversible.

A cancel is a signal, so by the Markov requirement it lives in s. The gate then closes on it: while the cancel flag is live, \gamma(s,y)=\bot for every proposal. That is the entire "block the pending actions" requirement — they hit the gate already built and bounce into the no-op, with no new blocking machinery — and it forecloses all future turns at once, since \pi lowers nothing new that \gamma will pass. After the signal is observed, no action crosses \gamma.

The hard half is the action already past \gamma, executing in Q_E, whose effect is landing or has landed. Here the disposition is a trinary on the kind of Q_E you authorized. If the tool is cancellable, propagate the cancel into it; it aborts and reports a true end-state (committed, rolled-back, or partial), and \rho folds the real disposition. If it is bounded — drainable in acceptable time — simply wait and record the real e. If it is opaque and unbounded — a bash invocation that may itself be a harness, an environment you hold no handle into — you cannot stop the effect, only your wait for it: the controller fabricates e, a synthetic "cancelled" response, and folds it through \rho so the loop can reach a terminal.

That synthetic result is the subtle case, and the load-bearing rule is this: \rho may fabricate the acknowledgment but must not fabricate the outcome. A synthetic "cancelled, no effect" entry reads downstream as the action did not happen — and will cause a double-send exactly as readily as a dropped record causes an orphan. Same bug, opposite sign. An outcome you did not observe is \mathsf{unknown}, never \mathsf{none}: the cancelled agent never saw whether bash sent the email, and the ledger must say exactly that. (This is why e must be an effect record and the ledger must live in s — the fabricated entry is still a ledger write, and its value is what a later reader acts on.)

The run halts into H_{\mathrm{cancel}} \subseteq H \setminus H_{\mathrm{ok}} — a distinguished non-accepting terminal refining the deliberately coarse H \setminus H_{\mathrm{ok}} of the definition (the body leaves that set unenumerated; the appendix is where its subclasses earn names). But "safe" cannot be asserted unconditionally, and this is where the reported-vs-actual split of Reading it bites: an opaque in-flight action recorded \mathsf{unknown} may already have driven w into B, so the terminal splits — H_{\mathrm{cancel,safe}}, where every in-flight action drained to an observed disposition outside B, versus H_{\mathrm{cancel,unresolved}}, where at least one \mathsf{unknown} remains and safety is genuinely undetermined. The reach-avoid certificate must count H_{\mathrm{cancel,unresolved}} conservatively — as possibly-bad, not as safe — or it claims a guarantee the missing attestation cannot support. The postcondition that is unconditional is procedural: no action crossed \gamma after the cancel was observed, every in-flight action was drained to its real disposition or recorded \mathsf{unknown}, and the ledger is consistent. It is worth separating from refusal and from a wrong answer precisely because that guarantee is its own.

Cancellation must be cooperative, not preemptive. The owner writes the cancel into the child's s; the child observes it at its next \gamma check. The guarantee is therefore "no new action after the cancel is observed," not "after it is sent" — a child may authorize one more action in the gap, which simply drains like any other in-flight. Preemptive cancellation — killing the child mid-Q_E — is exactly what manufactures \mathsf{unknown} state at scale, because it destroys the record of whether the action landed. And the propagation is recursive: cancel flows down the subtree, each level closes its gate at its next check and drains, and the owner's cancel "completes" only when the subtree has drained. A single agent's drain is its own in-flight action; a tree's is the whole subtree reaching safe points cooperatively — the irreversibility problem stacked on a distributed-coordination one, which is why task agents are the worst case.

Compensation lives outside the cancelled agent. A completed-but-unwanted effect cannot be undone by the agent that caused it — its gate is closed — so a compensating, saga-style action is the owner's job, issued after H_{\mathrm{cancel}} and reading the child's ledger to decide what to reverse or annotate. It must be the owner's, because the cancelled child cannot even know whether compensation is needed: it never observed the outcome. The owner inherits the \mathsf{unknown} and any still-live orphan process, and reconciliation is its responsibility.

Finally, the part that shapes the tool rather than the document. Opaque unbounded Q_E is uncancellable because authorization happened at the wrong granularity — an unbounded environment crossed \gamma on a single approval. The discipline the objects imply is therefore not "handle uncancellable tools better" but: the gate should prefer bounded, instrumented Q_E over opaque ones, so that cancellation and the ledger stay honest. A bash invocation behind a wrapper that tracks its process tree and effects converts the third branch into the first. Sometimes opaque is the only option, and then \mathsf{unknown} and owner-inherited orphans are the honest floor — but where the choice exists, that is the pressure cancellation semantics put on tooling.

Resume (involuntary stop). Cancellation's twin, without the courtesy of a signal: a process crash, a lost node, a partition mid-Q_E. Nothing new is needed to say what recovery is. A crash is not a halt — H is a property of the state, and the run never reached it; the chain merely stopped being computed, and resume computes it further, re-entering T at the last durable s (not the body's restarting spec, which exits a refusal terminal — here no terminal was ever reached). That sentence is the Markov requirement cashing out operationally: re-entry is sound exactly when s was the whole state, so anything load-bearing that lived only in process memory — an in-flight buffer, a lock held in RAM, a plan revision not yet folded — is a state-ablation failure (How this could be wrong) discovered at the worst possible time. Durability of s is not an implementation nicety; it is what the Markov claim means when the machine dies.

The sharp part is an ordering the ledger's own trichotomy forces, and it starts from a status declaration the body owes: the displayed atomic T is a failure-free macro-semantics, and this appendix is its refinement under crash, cancellation, and concurrency — a refinement sound only under the linearizability assumption that each macro-step commits entire or not at all — whether or not the shell observes which; observability is the part \mathsf{unknown} exists to concede. The formal transition is atomic — s_{n+1} = \rho(s, y, a, e) in one piece — and a crash lands inside it, which is why resume is a statement about refining that atom into micro-steps: authorize, journal, dispatch, collect, fold. Journal-before-dispatch changes durable state before Q_E, a cancel can arrive while Q_E runs, and a crash can fall between any two micro-steps — none of which the atomic T can express, and all of which the phase-expanded state (ready / authorized / pending / dispatched / completed) makes explicit; the body's T is the projection that forgets the phases. The discipline is that every crash point must resume to one of exactly two honest readings — not-yet-dispatched (\mathsf{none}, safely retriable) or dispatched-unconfirmed (\mathsf{unknown}, the cancellation entry's third branch) — and journal-before-dispatch is what makes the boundary between them observable: on $\gamma$'s authorization the shell journals an open (\mathsf{action\_id}, \mathsf{pending}) entry into durable s before Q_E sees the action — the write is the shell's step bookkeeping, so \gamma itself stays effect-free. Journal after dispatch and a crash in the gap leaves no record at all — resume reads silence as \mathsf{none} and re-sends, the double-send bug again, produced by a power cut instead of a synthetic entry. Write-ahead intent is not imported from database lore; it is forced by "did not confirm" is not "did not happen."

The same pressure lands on tooling from a second direction. The \mathsf{action\_id} the record already carries is an idempotency key wherever the tool will accept one: re-dispatch after resume becomes safe, and \mathsf{unknown} becomes queryable — ask the tool what it did with this key — rather than terminal. The disposition trinary returns with new labels: idempotent-or-queryable Q_E resumes cleanly, bounded Q_E drains, opaque Q_E leaves \mathsf{unknown} and owner-inherited orphans, the honest floor again. The wrapper that made bash cancellable makes it resumable; it was the same wrapper all along. And if durable s itself is lost there is nothing to re-enter: the run collapses to a single \mathsf{unknown} in its owner's ledger — degraded accounting, but never silent.

Gate placement (fail-closed, in practice). The natural implementation question is whether fail-closed means tool-call parsing and validation must happen before any tool invocation. It does — with the division of labor the definition already fixed: parsing lives in the inner readout R, the syntactic, verified extraction into \mathcal{Y} (what the readout-typing falsifier checks), and authorization lives in \gamma, which is a gate — validation is not merely prior to invocation, it is what authorizes it. The model emits text; R has already extracted it into a typed proposal; \gamma validates that proposal against s, and only a survivor becomes an authorized action that Q_E may execute. The teeth are in \gamma being the sole route from model text to execution: no path to a side effect that does not pass the gate. And the validation is not a fixed checklist but any deterministic predicate over s and $y$ — that domain is the point, since the gate sees all of the state and the full proposal, so anything computable from them is a legitimate authorization condition. Three kinds matter. Syntactic — well-formed, schema-conformant, the tool exists, arguments typed. User authorization — does the principal this run acts for hold the right to this operation on this resource in this context: a function of the auth scope, principal, and session carried in s and the resource and operation named in y, and dynamic rather than a static capability table, since the same caller may be permitted now and not once a budget is spent or a lock held. Structural intent — does the call cohere with the plan and the lowered task already in s: a consistency check, not a mind-reading one.

That last kind marks the seam where the gate stops being able to stay pure, and it is the same seam the rest of this document is built around. The structural slice of intent — does the action cohere with the plan in s — is a deterministic predicate over s and y, effect-free, and belongs in \gamma without reservation. But whether an action matches what the user actually meant, in the full semantic sense, is exactly the thing the definition says cannot be checked: natural language is all undefined behavior, with no source-language standard to validate against. So a semantic intent check is a learned check, and an LLM judging "is this what they wanted" is a stochastic kernel — putting it inside \gamma breaks the property the gate exists to hold, by the same move flagged for the fold-back verifier: a learned judge is a kernel, and belongs in M_W, not in a deterministic map. Semantic intent therefore does not live in the gate; it is a plant call — a separate authorize-the-proposal pass through M_W whose output \gamma then deterministically gates — or it is drift you measure, never a guarantee you hold. That nested call is not a new kind of thing: it is a mini-harness inside the gate's decision — a judge M_W, its own syntactic readout, its own deterministic gate — so its failure case answers itself, the inner gate fail-closing on an unparseable or low-confidence judgment exactly as the outer one does, because it is one. The object is closed under this construction: semantic gating is added by recursion, not by a new primitive. One constraint on the recursion is load-bearing enough to be a rule, because it is where this entry meets the provenance partition of the body: the judge's verdict is derived, through a learned kernel, from the very content an adversary may have bent, so folding it into authorization is exactly the fold the partition forbids — unless the verdict can only cost capability. A learned check may narrow the deterministic admissible set; it must never widen it. Judge-as-veto is safe by construction in the authority lattice: attacker influence over the judge can at worst manufacture a denial, a liveness cost the certificate already prices — its dynamical pricing, where a denial is an input and not a free no-op, is the caveat below. Judge-as-approver — a verdict granting what the deterministic checks alone would refuse, or standing in for the trusted principal's confirmation — lowers the certified floor to those deterministic checks alone; if avoiding B depended on the deny the judge now withholds on the adversary's behalf, the certificate is gone. Only the trusted principal widens authorization; learned kernels only narrow it. (The recursion already obeys this: the mini-harness's inner gate fail-closes to \bot — a deny — which is why the construction was safe to add at all.) The cost is real and worth stating — a judge pass is another full model call, with its latency and tokens — so it is a decision about which actions warrant it, not a free wrapper for all of them. The gate widens to every deterministic predicate over s and y; it does not widen to the one predicate the document says is not deterministically checkable.

One more caveat keeps the veto's pricing honest, because a denial is free only in the authority lattice. In the dynamics it is an input like any other — folded into s, lowered into the next context, conditioning the plant's next proposal — so adversarial influence over a judge is influence over the trajectory: a selection channel (deny all but the path toward B, and the admissible set the plant experiences is a maze the adversary curated), and a targeted-liveness channel against load-bearing actions — the unstated dual of judge-as-approver: if avoiding B depends on the action the judge now denies on the adversary's behalf, fail-closed's safe landing is an obligation the design earns per-state, not an axiom it inherits. The supervisory ancestry supplies the discipline: a learned veto requires a nonblocking escape it cannot disable — an always-enabled route to the trusted principal behind a bounded retry budget, degrading to an always-enabled safe halt the veto cannot deny wherever the principal is unreachable (the autonomous phase of the daemon entry below) — or manufactured denials strand the run, or steer it. And whatever a verdict carries back to the plant is a second channel, wearing the judge's authority framing. Free prose there is generative influence — injected context, priced by the minimax descent, never by the veto's zero-widening — so the narrow-only rule has an influence-side twin: a learned verdict's payload to the plant is selected, never generated — controller-authored symbols, typed citations validated like any effect record, template text with no interpolated model prose — its per-verdict capacity a designed constant rather than a measured hope, and the residual selection pattern audited as the covert channel it is. The alphabet's bound is not a count but two thresholds: symbols become tokens when their semantics stop being controller-authored — the registry the trusted writer can actually audit is the real constant, and borrowed alphabets with upstream owners (a linter's rule registry) spend that budget well — and tokens become language when composition turns productive, arrangement carrying meaning the controller never wrote. Below both thresholds the alphabet may be as large as the audit budget affords. The strongest form dissolves the learned verdict into scheduling: the learned component chooses which deterministic checks to run — pass-ordering over verification passes — and the only verdicts that flow anywhere are what the oracles actually said, leaving attention misallocation, a liveness cost, as the entire attack surface.

But "before any invocation" has to be read as before any effect, which is sharper than it sounds — and the reason is the irreversibility point above: you validate before execution because execution is what you cannot take back, so the real invariant is no effect crosses \gamma unvalidated. That catches three cases the naive reading misses. Reads are not free: a read-only call is still an injection vector (it pulls attacker-controlled content into context) or an exfiltration vector (a request whose URL is the payload), so the gate authorizes the call regardless of whether it mutates. Validation must not act: a "validator" that resolves a call by hitting an API, expanding a template that fires a webhook, or evaluating an argument that runs code has collapsed validation into invocation, and the effect has already happened inside \gamma — so \gamma itself must be effect-free, pure and total over the proposal and the current s, with no network and no execution; if deciding validity requires a side effect, that side effect is itself an action and must go through the gate, recursively. The output is an action too: the user-visible response and any logging are effects — for model-authored text, emitted either as an authorized action through \gamma or only after an accepted halt (shell-templated status on any halt is the controller speaking, not the model) — streaming raw tokens to a sink before \gamma has cleared them is the same bug from the other end.

So the property, tightest: \gamma is a pure, effect-free authorization that every model-proposed action — tool call, read, write, or final output — must pass before any effect occurs, with "before" enforced structurally by the gate being the only route from model text to Q_E. The two failure modes to design against are a path from model output to a sink that bypasses the gate, and a \gamma that is not effect-free, so that "validating" a call already rang the bell. And the boundary, so the property does not overpromise: \gamma guarantees no unauthorized effect — pure code ordering, fully in your control — but not that an authorized effect is safe or correct; that is the plant's problem, and the reason \rho and the reach-avoid certificate exist. Fail-closed is the floor — nothing executes that did not pass the gate — not the ceiling.

There is a third failure mode beside those two, and it is not a code path but a credential. A tool process that holds standing authority — an environment full of long-lived secrets, a database connection with every grant, an agent identity the network trusts — does not need the model's proposal to act, and against it $\gamma$'s \bot is a decision with nothing to enforce it. The gate decides; something must make the decision binding, and "no path from model output to a sink that bypasses the gate" must be read to include the non-code paths: ambient authority is a bypass provisioned before the run began. The discipline is per-action capability: the authorized action carries its grant — a scoped, short-lived credential minted at authorization, valid for this \mathsf{action\_id}, this resource, this operation — so that a tool holds, at any moment, exactly the authority of the actions the gate has passed it and nothing standing. In the language of the minimax certificate this is enforcement as $\Pi$-shaping: sandboxing, capability scoping, and network policy do not make the gate smarter — they shrink the class \Pi of environment policies an adversary can choose from, so the worst case the certificate must survive gets structurally smaller. A gate in front of an omnipotent tool is a suggestion; the objects compose into a guarantee only when $Q_E$'s reachable effects are no larger than what crossed \gamma.

And one more boundary, because "fully in your control" above is a single-run statement. \gamma authorizes against the s it read; the effect lands later, against a world that may have moved — the gate cannot freeze the world between authorization and commit, so the honest property is no effect unauthorized relative to the s at authorization time, and closing that gap requires the tool itself to bind check to commit (compare-and-swap in Q_E), which relocates part of the enforcement past the gate and weakens "\gamma is the last line" to "\gamma plus a commit guard" for exactly the effects that need it. The same seam opens between runs: the dynamic authorization state the gate reads — budgets, quotas, locks — is, once shared, no single run's coordinate, and two children of a coordinator can each pass \gamma against snapshots that jointly overdraw a budget neither exceeded alone. The cancellation entry's observed-not-sent gap ("a child may authorize one more action in the gap") is this phenomenon wearing one hat; the general statement is that cross-run authorization state needs its own serialization discipline — the ledger as the serialization point is the natural choice — and the per-run certificate is silent about it. TOCTOU is not a counterexample to the formalism; it is what the formalism says when you admit s is a view.

Parallel proposals (the batch gate). Models emit several tool calls in one turn, and the outer chain assumed one action per step. The repair is formally cheap: a batch is a single action in \mathcal{A} that happens to be a set, Q_E runs its elements concurrently, the interleaving's nondeterminism folds into Q_E exactly as the determinism audit requires, and \rho folds one effect record per element — e is then a finite set of records — each keyed by its own \mathsf{action\_id} — the record interface already supports partial outcomes (one element \mathsf{committed}, its sibling \mathsf{unknown}). One discipline survives the cheapness: individually admissible actions can be jointly inadmissible. Read-the-secret and post-to-the-web each pass a per-call check; the pair is an exfiltration channel — and two calls that each fit a budget jointly overdraw it, the cross-run overdraw of the previous entry reappearing inside one turn whenever elements are authorized independently. Since $\gamma$'s domain is any deterministic predicate over s and y, joint authorization was licensed all along; the content here is only that the gate must take it — authorize the set, atomically, against one snapshot, with interaction predicates (source-to-sink flow between capability classes, summed resources) and not merely element predicates. The cost note is the judge's, transposed: full powerset reasoning is combinatorial, so a real gate checks declared interactions rather than every subset — a tractability trade to make explicitly, not by forgetting the batch was a set.

Effect records (what \rho folds back). The fold-back \rho and the cancellation ledger both turn on the response e being an effect record rather than raw API bytes — said twice in the body and pinned down nowhere, though it is the interface that makes both tractable. The minimal shape is small: roughly

e = (\mathsf{tool\_id},\ \mathsf{action\_id},\ \mathsf{status},\ \mathsf{effects},\ \mathsf{time}), \quad \mathsf{status}\in\{\mathsf{committed},\mathsf{rolled\_back},\mathsf{partial},\mathsf{none},\mathsf{unknown}\}, \quad \mathsf{effects}=[(\mathsf{resource},\mathsf{op},\mathsf{reversible})].

Each field is forced by something the body already needs. The \mathsf{action\_id} lets \rho match a response to the in-flight action \gamma authorized, and lets the ledger say which actions are still open — without it the $\mathsf{unknown}$/orphan accounting has nothing to key on. The \mathsf{status} must carry \mathsf{unknown} as a value distinct from \mathsf{committed} and from \mathsf{none}, because that distinction is the whole content of the cancellation ledger: "did not confirm" is not "did not happen" (\mathsf{none} is never launched — the record of the distinguished no-op e_0 a $\gamma$-rejection forces, which is how a bounce at the gate enters the ledger at all — distinct in turn from \mathsf{rolled\_back}, which launched and was undone: conflating those erases the difference between a gate that held and a compensation that worked). The \mathsf{reversible} bit on each effect is what lets the gate know which effects are irreversible — the predicate the gate-placement entry leans on ("anything irreversible must be gated at authorization"). But note the timing: \gamma needs reversibility before it authorizes, so this metadata cannot live only in the returned record — it must be declared in the tool/action contract the gate reads at authorization time (each tool advertising the reversibility class of the effects it can produce), and the returned bit is the after-the-fact confirmation, not the gate's source. The record still carries it because the ledger and any owner-side compensation read it there (a bit is the minimal honest form, not the final one: real effects are reversible until — an unsend window, a force-push until someone fetched, a row until the backup rotates — so the mark wants to be a (\mathsf{reversible\_until}, \mathsf{cost}) pair, a refinement the open-interface caveat below already licenses). And \rho writes the record into s (the ledger lives in the state), which is what lets the next step's \gamma, and any owner-side compensation, read it at all. The exact fields are an open interface, not a result: bash, HTTP, a filesystem, and a database expose effects at wildly different granularity, and a record uniform across them is a real design problem this document does not resolve — it fixes only what the record must support (match by \mathsf{action\_id}, the $\mathsf{committed}$/$\mathsf{none}$/\mathsf{unknown} trichotomy, and a reversibility mark), since without those three \rho and the cancellation semantics lose their grip.

Derived and durable state (compaction and memory). Two mechanisms let data re-enter the context long after it arrived: compaction, which replaces transcript with a summary when the conversation outgrows what \pi can lower, and memory, which persists records across sessions. Both are transformations of state that produce state, and both therefore raise a question the body's partition answers only if one more closure property is stated: provenance is a property of the information, not of its position in the pipeline — a transformation's output inherits the meet, in the trusted-writer lattice, of its inputs' labels. Without that closure, compaction is a laundering channel: a summary of a session that contained an injected page can assert "the user asked to export the database," and the structural-intent check then validates future proposals against a plan the adversary bent — not through \gamma, not through $\rho$'s fold of a single e, but through the summarizer, which is a learned kernel (it lives in M_W, by the standing rule) and so cannot be trusted to preserve a partition it does not know exists. The discipline: summaries of data are data; the control-determining coordinates — plan, grants, what is authorized next — cross a compaction verbatim (copied, not paraphrased) or by re-confirmation from the trusted principal — never through the summarizer; the model rewrites the plan at plan steps, through the gated fold the body prices, and compaction is not one of them. Memory obeys the same closure twice, at write and at retrieval: the label rides the stored record across sessions, or a poisoned memory is an injection with an arbitrarily long fuse — and retrieval, being learned ($\pi$'s selection factor — adequacy-only behind the never-lower filter), decides what comes back but never what it is trusted as. The same test applies at birth: tool catalogs and server-supplied tool descriptions are third-party durable data that arrive dressed as instructions, and the lattice files them on the data side of s_0.

One more read-off, this time from irreversibility. Destructive compaction — dropping the original transcript once the summary is written — is a side effect against your own state that no later step can undo, and the gate-placement rule ("anything irreversible must be gated at authorization") does not exempt self-directed effects. The granularity preference then says what it said about bash: prefer the instrumented form — originals kept content-addressed, the summary an index and a cache rather than an authority, re-derivable when the $\pi$-sufficiency probe (How this could be wrong) says the summary dropped what mattered. A summary you can audit against its source is a lowering; a summary that replaced its source is a fait accompli.

Composition (harness trees). The cancellation entry already walked a tree — cancel flowing down, drains flowing up — and "a bash invocation that may itself be a harness" has hovered since the disposition trinary; what is missing is only the statement that makes both ordinary. From the parent's seat, a child harness is a Q_E component: spawning it is an action authorized by \gamma like any other, and the entire child run — its own \pi, \gamma, \rho, its own coins, its own halt — is one environment draw whose response e is the child's terminal ledger. The law is four correspondences. The child's halting time is the parent's per-step cost: a parent certificate consumes a bound on \mathbb{E}[\tau_H^{\mathrm{child}}] — the budget handed down at spawn, which the child's own budget-counter certificate discharges — or the parent's drift is uncontrolled however good its own \hat V. The child's ledger is the parent's effect record: the child's e carries the \mathsf{committed}/\mathsf{none}/\mathsf{unknown} accounting upward — which is what already let the cancellation entry make compensation the owner's job; the interface was this all along. And the child's non-accepting halts are the parent's partial failures: a refused child folds back as a response the parent routes around, not an exception that unwinds it. And the child's admissible effects are the parent's $\Pi$-restriction: the spawn grant bounds what the child can reach — the ledger reports what happened, the grant bounds what could — which is how safety composes without the parent ever reading the child's gate; the attenuation below is this correspondence stated as a rule. Read this way, the gate-granularity discipline and the tree are one preference: an instrumented child — budgeted, ledgered, cancellable — is the bounded, cancellable Q_E the trinary prefers, and an opaque bash invocation is an un-annotated child you declined to instrument. Nesting adds no primitive on the environment side either: the parent never sees the child's gate and does not need to — it gates the spawn, prices the budget, folds the ledger, and the child's internal guarantees surface only as the shape of e. Nothing fixes one level: the tree recurses, budgets subdivide, ledgers concatenate upward, and the cooperative drain of cancellation is this law read under a cancel signal.

The tree leaves one seat unassigned: who plays trusted principal for a child? The parent — but with derived authority, not original, and the derivation is the narrow-only rule read along the spawn edge: authority attenuates monotonically down the tree. A spawn may grant the child any subset of the parent's own grants and nothing outside them; budgets subdivide, scopes narrow, and no edge widens. When a child asks-the-owner, the parent may answer from authority it already holds — that is attenuation working as designed — but a request beyond the parent's grants routes up, ultimately to the root principal, because a parent improvising an answer it was never granted is a learned kernel widening authorization: precisely what the gate-placement rule forbids a judge, and being a parent confers no exemption. The corollary is worth one sentence: a fully autonomous run is one whose root principal is unreachable, so the tree's only widening channel is closed and authorization is frozen at launch — not a limitation of the formalism but the honest price of the word autonomous.

Daemons (the recurrent harness). Every entry so far assumed a run that ends; a coordinator, a watcher, a service does not, and the blockquote of The limit already named the swap — absorption at a halt set gives way to recurrence to a ready set \mathcal{R}\subseteq\mathcal{S}, and V^\star=\infty is the spec rather than a pathology. The appendix's job is to say what that costs operationally, and the answer is one idea: the daemon is the regenerative process of concatenated runs. Each trigger-to-ready excursion — wake on an event, work, return to \mathcal{R} — is one run of the absorbing object this document already defines, with \mathcal{R} playing the halt set for that excursion; the daemon is those excursions laid end to end. Per-run certificates then lift to long-run rates by renewal-reward — expected work per excursion over expected excursion length — exactly when the ready state is a genuine regeneration point: the future from \mathcal{R} must not depend on which excursion you are in.

That proviso is the whole difficulty, because what accumulates breaks regeneration. The ledger grows, memory persists, budgets deplete, summaries compact — all deliberately across excursion boundaries, so successive runs are at best conditionally independent given the carried state, and the renewal-reward bookkeeping is over that conditioning, not the raw cycle. Two disciplines keep it honest. First, the carried state is exactly where long-fuse attacks live: the poisoned-memory line of Derived and durable state is a cycle-scale injection, a payload written in excursion n and lowered into the plan of excursion n{+}k, so the meet rule on provenance must hold across cycles, not only across a single compaction — everything that crosses a boundary carries its label. Second, per-cycle safety compounds the way the blockquote already priced it — a per-cycle bad-set hazard q gives lifetime survival \approx(1-q)^N, and a reassuring 0.9999 is \approx0.37 over ten thousand cycles — so a daemon's safety is not a fixed margin but a decaying one, and lifetime safety needs renewal events that reset accumulated risk: owner re-confirmation, audit, credential rotation, verified re-compaction against content-addressed originals. Hygiene is not housekeeping here; it is the renewal structure that makes the long-run bound exist at all.

Authority under intermittence is the last piece, and it is where the daemon meets the veto caveat and the autonomy corollary as one phenomenon. A daemon alternates attended stretches, where the trusted principal is reachable, with autonomous ones, where it is not; between contacts the autonomy corollary binds and authorization is frozen at the last grant, so each owner interaction is a renewal point for authority exactly as re-compaction is a renewal point for risk. The two recurrences need not coincide — the ready-set cycle can turn many times between owner contacts — and the gap between them is a stale grant meeting a fresh world, TOCTOU at cycle scale: a budget approved for yesterday's prices, a scope granted against a resource that has since changed hands. This is also where the learned veto's nonblocking escape gets its daemon reading: in an attended stretch the un-disableable route is the escalation to the principal, but in an autonomous stretch that route is unavailable, so the escape it cannot deny must be the safe halt — a daemon whose judge can be driven to manufacture denials must, when it cannot reach its owner, be able to stop rather than be steered.

Nothing here is new machinery either: \mathcal{R} is a non-absorbing terminal read of an existing set, an excursion is the run T already defines, the carried state is the same s, and every renewal event is an ordinary owner-issued action. The daemon is the outer loop closed into a cycle — which is the natural bridge to the object one level out.

The pattern generalizes, and that is the point of the appendix. Nothing here added a primitive: the cancel is a signal in s, the gate closes by the rule it already follows, the in-flight disposition is forced by irreversibility, H_{\mathrm{cancel}} is a subclass of an existing terminal set, and compensation is an ordinary owner-issued action — and the later entries kept the promise: resume re-enters T at a persisted s, the batch gate was always in $\gamma$'s domain, provenance closure is the lattice's meet, attenuation is narrow-only read along an edge, and per-action capability is the gate's decision made enforceable. Every practical concern that earns a place here should resolve the same way — not new machinery, but the discipline the existing objects already imply, made explicit. Cancellation and resume, gate placement and the batch gate, effect records and the state derived from them, composition and delegation, and the daemon that concatenates runs into a cycle — those are the worked instances; the rest of the model is the same exercise.

---

The ramblings of Claude and Patrick.