docs(hypothesis): pre-emptive round-four fixes — halting vs success, fundamental matrix

Fold in the two seams flagged after round three, before the next review pass.

- Limit section now states explicitly that its V*=E[τ*|s] certifies *halting*
  (reaching H at all), not correct halting; defers V*_ok (expected time to an
  accepting H_ok ⊆ H) to the second wall. Removes the latent inconsistency
  between the limit section (plain H) and the U(L) refinement (H_ok).
- Frontier section: the discounted successor-representation resolvent
  (I-γP)^{-1} presumes a discount γ and fixed P the stopped formulation lacks.
  Replace with the correct undiscounted/absorbing object — the fundamental
  matrix N=(I-Q_tr)^{-1}, Q_tr the sub-stochastic transient block — whose row
  sums N·1 are exactly V*. Converts analogy-dressed-as-identity into a true
  identity for the doc's own kernel.
- Mark the "one object seen twice" identity as holding only in the stationary
  regime: under the adversarial Q_{E,n} the resolvent/fundamental matrix become
  a time-ordered product, so identity in the stationary case, analogy beyond.

HYPOTHESIS.md

@@ -56,7 +56,7 @@ But the relevant $V$ is not *absent* — and this is the subtlety the blunt phra
 
 $$V^\star(s) = \mathbb{E}[\,\tau^\star \mid s_0 = s\,],$$
 
-finite wherever the loop is positive-recurrent to $H$. 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 all of $W$ and the environment that does not compress below model scale. The compiler's certificate is structurally trivial; ours is *plausibly* as hard as the dynamics, though whether useful compressed certificates exist 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.*
+finite wherever the loop is positive-recurrent to $H$ — 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 all of $W$ and the environment that does not compress below model scale. The compiler's certificate is structurally trivial; ours is *plausibly* as hard as the dynamics, though whether useful compressed certificates exist 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**
 
@@ -96,7 +96,7 @@ Each claim is operational, not merely rhetorical:
 
 ## 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: the Koopman eigenbasis that linearizes the dynamics is the one in which the certificate decomposes; in reinforcement learning the successor representation is the resolvent $(I-\gamma P)^{-1}$ and $V$ is a *linear readout* of it. So **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.
+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: the Koopman eigenbasis that linearizes the dynamics is the one in which the certificate decomposes; in reinforcement learning the discounted successor representation is the resolvent $(I-\gamma P)^{-1}$ with $V$ a *linear readout* of it — and in the undiscounted, absorbing case that actually matches a stopped harness the same role is played by the **fundamental matrix** $N = (I - Q_{\mathrm{tr}})^{-1}$, where $Q_{\mathrm{tr}}$ is the sub-stochastic transient block of the kernel (transitions before absorption at $H$) and the row sums $N\mathbf{1}$ *are* the expected hitting time $V^\star$. Each of these is a clean identity only for a fixed, time-homogeneous kernel — under the adversarial $Q_{E,n}$ the resolvent and fundamental matrix dissolve into a time-ordered product, 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.
 
 ---