From 6c32b7e3cf0bcfa515e200f7e331d3aa7614b0cd Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 22 Jun 2026 19:08:13 +0000 Subject: [PATCH] =?UTF-8?q?docs(hypothesis):=20round-eight=20micro-edits?= =?UTF-8?q?=20=E2=80=94=20precise=20compiler=20claim,=20well-posedness=20w?= =?UTF-8?q?ording?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The review's verdict was "Merge." These are its two correct non-blocking nits; its third nit (stop adding theorems/caveats) is heeded — nothing else changed. - Grounding: "the compiler's V is free" → "a classical monotone data-flow analysis gets its V for free." A whole compiler does not get termination for free; the specific lattice-based analysis does (Kildall). - Asserted: the Koopman/certificate co-determination "holds only under" → "is well-posed only under" the spectral assumptions — avoids asserting truth ("holds") for a claim explicitly labeled as not-a-theorem. Deliberately NOT changed: D → D_H (prose already marks D harness-relative; subscripting one formula while D stays bare elsewhere would add asymmetry, not remove it), and no further theorem additions or caveats per the review's note that more caveating now costs clarity without adding rigor. --- HYPOTHESIS.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/HYPOTHESIS.md b/HYPOTHESIS.md index 7681f9d1..ba661368 100644 --- a/HYPOTHESIS.md +++ b/HYPOTHESIS.md @@ -108,9 +108,9 @@ With that caveat, **the interlingua and the certificate are one object seen twic Borrowed theorems are real; the framings are not — keep them separate. -**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). 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 verify a candidate $\hat V$ by its measured drift rather than deriving $V^\star$ (neural-Lyapunov: Chang, Roohi & Gao, *Neural Lyapunov Control*, NeurIPS 2019, arXiv:2005.00611). The compiler's $V$ is free because a finite-height lattice is a well-founded descent (Kildall, POPL 1973). Dialect-stack architecture: MLIR (Lattner et al., CGO 2021, arXiv:2002.11054); learned pass-ordering: MLGO (Trofin et al., arXiv:2101.04808). Single-pass constant-depth under fixed-depth/fixed-precision assumptions: the $\mathsf{TC}^0$ transformer-expressivity results (Merrill & Sabharwal) — with the caveat that log-depth and growing-precision variants change the picture, so the bound is suggestive for deployed models, not literal. +**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). 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 verify a candidate $\hat V$ by its measured drift rather than deriving $V^\star$ (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). Dialect-stack architecture: MLIR (Lattner et al., CGO 2021, arXiv:2002.11054); learned pass-ordering: MLGO (Trofin et al., arXiv:2101.04808). Single-pass constant-depth under fixed-depth/fixed-precision assumptions: the $\mathsf{TC}^0$ transformer-expressivity results (Merrill & Sabharwal) — with the caveat that log-depth and growing-precision variants change 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* — including the Koopman/certificate co-determination, which holds only under the spectral assumptions noted there, and the interlingua/certificate identification. These organize the design; they are not results. +**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* — including the Koopman/certificate co-determination, which is well-posed only under the spectral assumptions noted there, and the interlingua/certificate identification. These organize the design; they are not results. ---