docs(hypothesis): round-three review fixes — V*_ok vs V*, pushforward readout, tool discharge

Address the round-three review. The substantive one is the V* correction.

- Successful halting vs raw halting (the real conceptual fix): a U(L) task does
  NOT make V*=E[τ_H|s] undefined — the chain can still hit H by failing closed,
  refusing, or returning a wrong answer. Split H from the accepting set H_ok and
  define V*_ok=E[τ_{H_ok}|s]; U(L) blows up V*_ok, not V*. Restate the domain as
  dom_{<∞}(V*_ok) ⊆ reachable(L)\D.
- Tools compute, not just store: the L-wall binds *model-mediated* work; work
  discharged to a verified external tool (solver, interpreter, compiler) runs
  off-context. U(L) now excludes tool-dischargeable work explicitly.
- Readout typing: use the pushforward M_W(c,·)=R_# Law(c_τ) (equivalently the
  conditional law); make R total, R: C → Y_⊥, with the ⊥ branch handled by the
  fail-closed ρ.
- Adversary/history: a history-conditioning adversary needs that history in s,
  else the object is a Markov game requiring further augmentation, not a chain.
- Hedge the LBA claim: "in the variable-L, fixed-precision idealization, the
  model-mediated inner computation behaves like a linear-bounded automaton."

HYPOTHESIS.md

@@ -14,13 +14,13 @@ Most descriptions of an agent framework are a feature list. This is an attempt a
 
 $$T(s, A) = \int_{\mathcal{Y}\times\mathcal{E}} \mathbf{1}_A\!\big(\rho(s, y, e)\big)\; M_W(\pi(s), dy)\; Q_E(s, y, de),$$
 
-and the harness runs $s_{n+1} \sim T(s_n)$ until $\tau^\star = \inf\{n : s_n \in H\}$. Because $\pi, \rho, H$ are deterministic they sit *outside* the integral: 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.) 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.
+and the harness runs $s_{n+1} \sim T(s_n)$ until $\tau^\star = \inf\{n : s_n \in H\}$. Because $\pi, \rho, H$ are deterministic they sit *outside* the integral: 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.) 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.
 
 *The inner kernel.* $M_W$ is itself a stopped process, and for a decoder-only transformer it is implemented as
 
 $$M_W(c) = \mathrm{Law}(c_\tau), \qquad c_{t+1} \sim K_W(c_t, \cdot), \qquad K_W(c,\, c\!\cdot\! v) = (U \circ \Phi_W \circ \mathrm{Emb})(c)[v],$$
 
-with the layer stack $\Phi_W$ on the residual stream as the "manifold" core. Here the output space $\mathcal{Y}$ is either the stopped context $c_\tau$ itself (so $\mathcal{Y} = \mathcal{C}$) or a deterministic readout $R(c_\tau)$ — a parsed tool-call, answer, or transcript — in which case $M_W(c, dy) = \mathrm{Law}\big(R(c_\tau) \in dy\big)$; that reconciles the kernel $M_W(c, dy)$ into $\mathcal{Y}$ with the law $\mathrm{Law}(c_\tau)$ over contexts. 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.
+with the layer stack $\Phi_W$ on the residual stream as the "manifold" core. Here the output space $\mathcal{Y}$ is either the stopped context $c_\tau$ itself (so $\mathcal{Y} = \mathcal{C}$) or a total readout $R : \mathcal{C} \to \mathcal{Y}_\bot$ — a parsed tool-call, answer, or transcript, returning $\bot$ when parsing fails — in which case $M_W(c, \cdot) = R_\#\,\mathrm{Law}(c_\tau)$, the pushforward of the stopped-context law along $R$ (equivalently $M_W(c, B) = \Pr[R(c_\tau) \in B \mid c_0 = c]$). That reconciles the kernel into $\mathcal{Y}$ with the law over contexts, and the $\bot$ branch is exactly what $\rho$ 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.
 
@@ -72,7 +72,7 @@ $$\sup_{e\,\in\,E_{\text{adm}}}\ \mathbb{E}[\,V(s_{n+1}) \mid s_n,\, e\,] \le V(
 
 a descent that must hold even when the environment picks the worst admissible step. A $V$ that certifies halting against a benign world is defeated by an adversarial one, and the measured $\delta$ bounds only the $E$ you *sampled*, never the $E$ an attacker will choose. **This is the formal home of prompt injection** — not "the model did something bad," but the environment optimized to break your descent. It is also what fail-closed verification ($\rho$) is *for*: the disturbance-rejection margin that caps how far an adversarial world can move the drift. In this language, security is robustness of the certificate.
 
-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. Under the standard fixed-depth, fixed-precision theoretical model a single forward pass is constant-depth ($\mathsf{TC}^0$) — *suggestive* for deployed models, not literal, and shifting once depth grows with context (log-depth variants escape parts of it); the qualitative point survives the caveats: one pass buys bounded sequential depth, so the loop buys more only by emitting tokens: **the context window is the tape, the autoregressive loop is the read/write head**, and the inner solver is a linear-bounded automaton — its reachable fixpoints capped by space-$O(L)$ computability (chain-of-thought is register-spilling onto that tape). This is a *second* non-haltable region beside the divergent set: $U(L)$ — not tasks whose *data* exceeds $L$ (those the shell can page) but tasks whose **irreducible per-step working set** exceeds $L$, so they cannot be decomposed into $\le L$-resident steps even with paging; $V^\star$ undefined not because the loop diverges but because the live computation was never expressible in $O(L)$ space. So $\mathrm{dom}(V^\star) \subseteq \mathrm{reachable}(L) \setminus D$. The two walls **trade**: parametric memory $|W|$ and working memory $L$ are substitutable on one budget line — the pretraining-vs-inference-scaling axis. And the bound is inherent to *finite working memory*, not attention specifically: state-space models make it **tighter** (a fixed register set), and real attention's usable tape is shorter than $L$ (lost-in-the-middle).
+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. Under the standard fixed-depth, fixed-precision theoretical model a single forward pass is constant-depth ($\mathsf{TC}^0$) — *suggestive* for deployed models, not literal, and shifting once depth grows with context (log-depth variants escape parts of it); the qualitative point survives the caveats: one pass buys bounded sequential depth, so the loop buys more only by emitting tokens: **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). This is a *second* obstruction beside divergence, and it concerns *success*, not raw halting. Split the terminal set: let $H$ be any halt/ready 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]$. Then $U(L)$ 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(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 or semantically undefined. The honest statement is about the finite-success domain: $\mathrm{dom}_{<\infty}(V^\star_{\mathrm{ok}}) \subseteq \mathrm{reachable}(L) \setminus D$. The two walls **trade**: parametric memory $|W|$ and working memory $L$ are substitutable on one budget line — the pretraining-vs-inference-scaling axis. And the bound is inherent to *finite working memory*, not attention specifically: state-space models make it **tighter** (a fixed register set), and real attention's usable tape is shorter than $L$ (lost-in-the-middle).
 
 ## Where it cashes out