Review follow-ups: the s-shorthand convention and its glossary echo now
cover Q_E's own state argument (s -> w where Q_E reads it), and the Q_E
glossary row carries the factored (w, a) ~> (w', o) reading so the
symbol table no longer reintroduces the environment-reads-all-of-s
interpretation the outer-kernel note warns against. PRIMER: the
top-alone-widens bullet keeps owner language anchored to the
simple-case top; success is defined as an accepted end, consistent
with the declared-vs-actually-right distinction two sentences later.
HYPOTHESIS.md:
- carry the initial law mu_0 in the tuple (and its displayed signature);
split the rejection symbol into parse failure vs authorization
refusal, with gamma(s, bot_Y) = bot_A as an axiom and a positional
convention for the remaining bare bots
- factor the state s = (q, w) and retype Q_E to (w, a) ~> (w', o) so the
latent world has a generator and the displayed T is its stated
projection; quantify fail-closed over a rejection-invariant safe set K
- read H_ok as operational acceptance (H_acc) against analysis-only
success G, with a convention for which claims read which side; score
C6's ceiling against G and pin C5's slack to the correct-halting
drift, resolving the tension with its own falsifier
- state ledger integrity relative to an attestation assumption (reported
vs actual effects); split cancellation into safe vs unresolved and
count unresolved as possibly-bad; add the realizability clause to
C1/C3; admit multi-principal trust tops as deployment choices
- reversibility is declared in the tool contract the gate reads at
authorization; the returned record's mark is confirmation, not source
PRIMER.md: mirror the same corrections in plain language -- ceiling not
cliff for the desk wall, contract-first reversibility, the multi-party
trust top (including the summary line), declared-vs-actual success on
dashboards, reported-vs-actual ledger honesty, cancel is not
automatically safe.
HYPOTHESIS.md:
- New appendix entry "Daemons (the recurrent harness)": a daemon as the
regenerative process of concatenated runs — ready-set recurrence,
renewal-reward lifting exactly at regeneration points, accumulation as
what breaks regeneration (cross-cycle provenance meet, renewal events
that reset accumulated risk), and authority under intermittence
(owner contact as a renewal point for authority; TOCTOU at cycle
scale).
- New body section "The loop": the task-dispatching outer loop as the
harness construction applied one level out — the composition
correspondence read at the top level, the daemon as its single-agent
special case, the bare while-loop as the trivial-group harness one
level up. Flagged as a sketch; outer fail-closed/reach-avoid
treatment deferred to later rounds.
- Veto caveat threaded to match: judge-as-veto safety scoped to the
authority lattice, and the nonblocking escape degrades to an
always-enabled safe halt when the principal is unreachable.
- Consistency: Grounding's Asserted tier now covers "The loop";
"always-enabled escalation" -> "escape" (the appendix's own term, now
that the escape has an unattended form); brace the one unbraced \bot
subscript (linter section-B HIT).
PRIMER.md: new plain-language companion — same object, no symbols, the
formal doc wins every disagreement. README's entry link now points at
the primer, which links onward to HYPOTHESIS.md.
- Proven: name supervisory control's controllability and nonblocking
conditions as the ancestors of gate-early-on-irreversibles and the
always-enabled escalation required behind a learned veto; cite TCSEC
covert-channel analysis (NCSC-TG-030) for the verdict channel.
- Asserted: add the narrow-only rule's influence-side twin (verdict
payloads to the plant selected, never generated).
- New caveat paragraph: a denial is free only in the authority lattice;
in the dynamics it is an input (selection + targeted-liveness
channels), so a learned veto needs a nonblocking escape it cannot
disable, verdict payloads are selected rather than generated with the
symbols/tokens/language thresholds bounding the alphabet, and the
strongest form dissolves the verdict into scheduling over
deterministic checks.
Corrections: the middle-form re-separation names its true mechanism
(restarting specs or refusal-event predicates; within-run retries never
touch F), the standard-Borel aside admits belief-state coordinates, the
drift-slack display binds its variable, effect-record status gains a
`none` value (never launched) distinct from rolled_back and unknown,
and parsing is assigned to the inner readout R with the gate as pure
authorization.
Structure: the trusted principal as the provenance lattice's single
widening writer; two-rank control (authority vs plan) with a
rank-neutrality corollary; the narrow-only rule for learned checks;
pi's never-lower filter joins the deterministic core; gate TOCTOU and
cross-run serialization; a composition law for harness trees (four
correspondences) with delegation as monotone attenuation.
Appendix: new worked entries for resume (journal-before-dispatch),
parallel proposals (the batch gate), derived and durable state (the
provenance meet rule), and ambient authority (per-action capability).
Claims numbered C1-C8; two falsifiers added (certificate compression;
working-set probe anchored in streaming lower bounds).
Grounding: adds Ramadge-Wonham supervisory control, RL shielding, and
Dayan's successor representation; repairs the Positivity/Skolem gloss
and two citation characterizations. All 18 external citations verified
against their sources.
- Add a plain-terms gloss of the claim (shell/plant split up front)
- Add a 'Converged-upon' grounding subsection: independent corroboration
from capabilities, control theory, software architecture, and LM theory
- State provenance as a precondition of the reach-avoid certificate
(CaMeL control/data-flow separation), not just an entry point to police
- Drop redundant 'none' from the effect-record status enum; normalize
minor notation (A_bot, h->N)
- Fix stray backslash-escaped quotes that rendered literally
* docs(hypothesis): gate-placement & effect-record appendix; scope incompressibility; split the two walls
Refinement + expansion pass on the harness hypothesis.
Appendix (new subsections):
- Gate placement (fail-closed, in practice): γ as a pure, effect-free
parse-and-authorize; syntactic / user-authorization / structural-intent
validation; semantic intent as a recursive plant call (a mini-harness),
not a predicate in γ; "before any invocation" sharpened to "before any
effect" — reads aren't free, the parser must not act, the output is an
action too.
- Effect records (what ρ folds back): pins down the
e = (tool_id, action_id, status, effects, time) shape the body referenced
twice but never defined; committed/none/unknown trichotomy + a reversibility
bit, framed explicitly as an open interface, not a result.
Corrections:
- Scope the incompressibility conjecture: split per-step drift by coordinate
(the shell term is a low-complexity designed descent), so the incompressible
part is the plant's, not all of W; add the coarse-functional counter-
possibility (V* is one scalar hitting time, sometimes cheap) and state the
claim conditionally. Walks back the earlier "the dynamics it certifies are
the weights" overclaim.
- Split the second wall: the tape / space-O(L) picture follows from the
autoregressive structure alone; the per-pass TC^0 bound is separate and
weaker; flag that chaining them is a non-sequitur.
Smaller:
- Concrete justification for the standard-Borel assumption.
- Reading-table rows for the C/Y/A/E spaces and for H_ok/B.
- Daemon note: per-cycle hazard compounds, (1-q)^h over the horizon.
- Minimax: well-posedness caveat for sup over the adversary class Π.
- Note that H_cancel refines the body's deliberately coarse H\H_ok.
Notation (consistency linter clean):
- Brace the subscript A_{⊥} in the new table row (was unbraced — GitHub
render hazard the linter guards against).
- Daemon cycle-count N → h, freeing N for the fundamental matrix.
* docs(hypothesis): address Copilot review — plain quotes + 'none' status value
- Effect-record status enum: add `none`, which the prose already treats as a
distinct value ("unknown ... never none"; the committed/none/unknown
trichotomy). Resolves the enum/prose inconsistency — `none` (no effect) is
distinct from `rolled_back` (ran, then undone).
- Drop the two backslash-escaped quotes (the incompressibility walk-back and
the minimax well-posedness caveat) for plain quotes, matching the rest of
the document. GFM strips the backslash, so they rendered fine; the escapes
were just unnecessary and inconsistent.
* docs(hypothesis): clarity pass, GitHub-render fixes, consistency linter
Document (HYPOTHESIS.md):
- split the dense "Formal" definition into labeled subsections
- define the load-bearing terms: certificate (proven witness vs measured
surrogate) and the controller / plant (= M_W) / shell triad
- corrections: three-way drift split (+ r_env), scope the success/safety
collapse to absorbing refusal, unify tau*->tau_H and drop the orphaned bare tau
- calibrations: pin the incompressibility conjecture (still conjectural),
mark the interlingua=certificate identity as figure, soften the two-walls trade
- GitHub math rendering: brace command-subscripts (_\bot -> _{\bot}, etc.) so the
markdown emphasis parser stops breaking inline math; replace R_\# with R_{\sharp}
(\# unescapes to a raw # in GitHub math)
Linter (lint_hypothesis.py):
- deterministic consistency checks A-G; G adds an orphan/redundant-declaration
scan that catches the bare-tau failure mode
- residue guards so tau^star, unbraced _\cmd subscripts, and \# cannot return
* fix(hypothesis): make lint_hypothesis.py pass ruff under py311
- precompute the inline-$ count so no backslash sits inside an f-string
expression (backslashes in f-strings are 3.12+; the project targets 3.11)
- split the one-line import (E401/I001); open HYPOTHESIS.md via a context manager (SIM115)
Establishes the appendix pattern (locate a practical concern in the existing
formal objects; read off the discipline rather than inventing machinery) with
cancellation as the first and only worked example. Not the whole model.
Cancellation semantics, derived from objects already on the page:
- Cancel is a signal → lives in s (Markov). The gate closes on it: γ(s,y)=⊥ while
live, which blocks pending actions and all future turns with no new machinery.
- In-flight (past γ) disposition is a trinary on the kind of Q_E: cancellable
(propagate, true end-state), bounded (drain, real e), or opaque/unbounded
(controller fabricates a synthetic "cancelled" e so the loop can halt).
- Load-bearing rule: ρ may fabricate the acknowledgment but not the outcome — an
unobserved outcome is `unknown`, never `none` (double-send vs orphan, same bug
opposite sign).
- New terminal H_cancel ⊆ H\H_ok: non-accepting but safe (outside B), postcondition
"no action past γ after observed; in-flight drained or recorded unknown; ledger
consistent."
- Cooperative not preemptive (observed at next γ check, not on send); recursive
down the task-agent subtree (why task agents are the worst case).
- Compensation is the owner's job (saga, after H_cancel, reads child ledger) — the
cancelled agent can't know if it's needed; it never observed the outcome.
- Design pressure: prefer bounded/instrumented Q_E over opaque, so cancellation and
the ledger stay honest (a bash wrapper converts branch 3 -> branch 1).
Linter: balanced, no new collisions. Two ρ role-flags, both false positives
("authorized action" near ρ, correct usage).
The linter closed mechanical consistency; this review probes meaning, a separate
axis. Twelve findings, several real corrections, all folded.
Correctness:
- Stationarity overclaim: the supermartingale BOUND survives a nonstationary
kernel under uniform conditional drift. Time-homogeneity is needed for V* as a
fixed function, the resolvent/fundamental-matrix identities, and δ-calibration.
- Self-contradiction: "the certificate cannot be proven, only observed" contradicted
the established "a proven inequality certifies" — reworded to "the architecture
does not hand it to you; estimated unless separately certified."
- Citation: the TACL result is LOG-precision → logspace-uniform TC⁰ (verified);
fixed/constant precision is a stronger restriction. Fixed in body and Grounding.
Modeling holes closed:
- Adversary class Π must respect rejection: γ(s,y)=⊥ ⇒ Q_E^α(s,⊥,·)=δ_e0, else the
adversary resurrects refused side effects.
- R must be a syntactic/verified readout, not a semantic solver — otherwise the
L-wall is void (compute could hide in R off the ≤L window).
- e must be an effect record (ledger outcome), not just API bytes, since only ρ
writes external effects into s.
- The displayed M_W(c) freezes endpoint/version/sampler; config changes need a
state-indexed M_{κ(s)} or K_C — the kernel can't silently depend on config in s.
- The final user-visible response/log is itself an effect: an authorized action
through γ, or emitted only after an accepted halt.
- m_t must include a token counter and clock for the cap/timeout to be functions of it.
Residue (omissions a collision-linter can't catch):
- Another γ dropped from the K_C Dirac-special-case list.
- τ* mislabeled as "designed code" → the halt test (H) is the code; τ* is its
emergent hitting time.
- H\H_ok relabeled "non-accepting" (safe refusals outside B; wrong/bad halts
possibly in B), not uniformly "rejecting/fail-closed."
Built and ran a static linter (no model): delimiter/emphasis balance, residue
regexes for everything prior rounds fixed, single-capital collision scan, a
definition check for recently-introduced symbols, and a γ/ρ role-neighborhood
scan. Result:
- All balance checks pass; all 10 residue regexes clean (no regression across
14 rounds); all 12 introduced symbols defined; no display-only symbols.
- γ/ρ scan: one flag, a false positive (the symbol-table cell defines both).
- One real find: G was overloaded — the parser-stop update G(m_t,v) (added in
round 14) collided with the Green/potential operator G. Renamed the stop-update
to \mathsf{step}; the Green operator G is now unique.
This closes the consistency axis deterministically rather than by another review.
Same prior-maxima full-tools review, re-run. Found mostly residue from round-13's
own edits plus longer-standing inconsistencies. Folded all; left the final
signature line alone (it is the author's call, and it is well-formed — see below).
Round-13 residue:
- 𝒴/𝒴_⊥ split half-committed: 𝒴 already includes ⊥, so R:𝒵→𝒴 and A_Y⊆𝒴 (drop _⊥).
- m_t was added to the inner triple with no dynamics: add m_{t+1}=G(m_t,v), define
the stop set Stop and τ=inf{t:m_t∈Stop} in both display and prose.
- No-truncation special case had R=id, ill-typed on a triple: R(c,b,m)=c.
- Safety/success "exactly on safe refusals" overclaimed: they differ on any
B-avoiding non-success run — also safe non-halting / endless safe retry, absent
a.s. absorption into H∪B.
Role residue (γ does authorization/rejection; ρ does response/fold-back):
- "⊥ branch is what ρ rejects" → γ rejects it.
- "ρ validates response as well as the proposal" → ρ validates the response; γ
gated the proposal.
- "fail-closed rejection at ρ" (falsification list) → at the gate γ.
- Symbol table still typed Q_E on authorized a → a∈𝒜_⊥ with the no-op; define e_0.
Longer-standing:
- Stochastic-controller contradiction: stochastic control falsifies the
deterministic special case, not the broader K_C kernel model (round-9 K_C).
- Drift split r=r_shell+r_plant needs an additively separable V̂ or a declared
attribution scheme.
Citation (verified via search, not the reviewer's say-so):
- TC⁰/log-precision → Merrill & Sabharwal, "The Parallelism Tradeoff", TACL 2023;
caveat (added autoregressive steps escape it) → Merrill & Sabharwal, "The
Expressive Power of Transformers with Chain of Thought", ICLR 2024.
A cold reviewer given the complete prior-maxima changelog + full tools ran a
consistency audit of the file (it did not use tools for grounding — the gap was
internal). Found 15 real issues, all folded. No new design flaws; this is
accumulated editing debt from 12 rounds of surgical patches.
Half-applied fixes now propagated:
- Inner-kernel display still showed M_W(c)=Law(c_τ) and R:C→Y_⊥ despite the round-12
triple; made z_t=(c_t,b_t,m_t) primary, R:Z→Y_⊥, M_W=Law(R(z_τ)).
- Append formula still used bare c·v; now suffix_{≤L}(c·v) in the display.
- Tuple still called B a "terminal set"; B is separate (τ_B fires mid-run).
- "halt/ready" survived at line 75 (fixed before only in tuple + table).
Collisions created by added notation:
- γ was both the authorization gate and the RL discount in (I-γP)^{-1}; discount → β.
- B was both the bad set and the dummy measurable set in the pushforward; dummy → A_Y.
- ρ over-credited as the disturbance-rejection margin; for side effects the margin
is γ (consistent with round-12 irreversibility), ρ validates response/fold-back.
Real error in a prior round:
- The round-12 safety/success distinction collapses under absorbing refusal
(Pr(τ_Hok<τ_B) requires reaching H_ok, so it is a success form). Split correctly:
p_succ=Pr(τ_Hok<τ_F), F=B∪(H\Hok); p_safe=Pr(τ_B=∞); they differ on safe refusals.
Typing / hygiene:
- Q_E typed on S×A_⊥ (it is applied to ⊥); 𝒴 declared to include ⊥ (M_W, γ total).
- Controller list omitted γ and mis-listed the readout (specialization-only).
- Defined the previously-bare symbols D={s:E[τ_H]=∞}, μ, the drift r(s), and Π.
- Grounding "verify by measured drift" overstated; a proven inequality certifies,
empirical drift only checks — reconciled with the body.
A cold no-priors review (given a local sandbox it did not use — the remaining
work is judgment, not computation). Mostly editorial/formal; its real catches
again concern round-10/11 additions. Folded the substantive ones, declined the
"extract a smaller core" restructure and the formalism padding.
Substantive:
- Inner kernel: replace round-11's awkward "read c_τ as the buffer" overload with
a clean inner-state triple z_t=(c_t,b_t,m_t) — window, output buffer, parser/
stop state — and M_W(c,·)=Law(R(z_τ)) from z_0=(c,∅,m_0). Strictly cleaner.
- Authorization is the irreversibility boundary: ρ can reject a bad tool RESPONSE
but cannot undo an authorized action's side effects, so γ (not ρ) is the last
line before irreversible effects. And the gate is bypassed if raw y reaches any
sink (tool, logger, browser, remote) before γ.
- Safety ≠ success: p_ok=Pr(τ_Hok<τ_B) is the safety object (refusal permitted);
the stricter success object races H_ok against all failure F=B∪(H\Hok). They
differ exactly on safe refusals.
Precision:
- Foster–Lyapunov positive recurrence needs irreducibility/petite-set hypotheses;
the absorbing-halt case needs only the weaker supermartingale hitting-time bound.
- Name an initial distribution s_0~μ_0. Fix residual "halt/ready" in the table
(round 11 fixed only the tuple).
A JSON-constrained cold review largely validated round 10; its new catches
cluster in round-10's newly-added material.
Fixes (the real ones):
- Terminal-set partition was wrong (a round-10 error): B is NOT a terminal
component — τ_B can fire mid-run. H now splits into accepting (H_ok) and
rejecting/fail-closed (H\H_ok); B is a separate unsafe set for reach-avoid.
- Fail-closed generalized: rejection need not be terminal (reject-then-retry is
valid) — define it as "no unauthorized side effect + land in a safe non-bad
set," with terminal rejection one case. ρ must also validate the tool RESPONSE
e (adversarial/malformed Q_E output), not only the model proposal at γ.
- Sliding-window truncation (round-10) loses transcript: the readout R reads a
separate output buffer, not the truncated c_τ alone.
Precision:
- Deterministic maps are measurable transforms inside the pushforward, not
literally "outside the integral."
- Absorbing halt H vs the separate (non-absorbing) daemon "ready" recurrence.
- "Syntactic soundness is free" qualified: relative to a formal schema and a
correct validator.
- State-ablation falsifies Markovity but cannot establish it (necessary, not
sufficient). Added a readout-typing diagnostic.
A cold no-tools external review (lower trust on world-facts, but its catches are
math-internal and correct) found two real bugs plus rigor gaps.
Bugs fixed:
- Verification-after-side-effect (the important one): the kernel ran e~Q_E(s,y)
then ρ verified, so a tool call's side effect landed before authorization. Add
a deterministic authorization gate γ:S×Y→A_⊥ between model and environment;
Q_E now acts on the authorized action γ(s,y); ρ becomes ρ(s,y,a,e). Fail-closed
is now a property (γ=⊥ ⇒ no-op env ⇒ fold to H\H_ok), not a name.
- Minimax drift display had a free y (introduced round 9): it integrated only
over e while y~M_W(π(s)). Now integrates over both y and e, adversary as a
policy α(s,y) over environment kernels, on the authorized action.
Reframing / rigor:
- Raw halting is cheap: a budget counter k gives V=k as a trivial halting
certificate, so "no certificate by construction" overstated. The missing
guarantee is correct/safe/successful halting (H_ok, B, p_ok).
- Standard Borel spaces (not merely measurable); define H, H_ok (⊆H), B (∩H_ok=∅)
and hitting times τ_A up front; add 𝒜 to the tuple.
- Inner kernel: truncate c·v to suffix_{≤L} at the window edge; M_W is a
probability kernel only via EOS/max-token/timeout/⊥ (else sub-probability +
cemetery).
- Drift: weaker bound δ≤δ̄<ε gives E[τ]≤V̂/(ε-δ̄); distinguish δ_ν (distributional)
from δ_sup (worst-case).
- Injection enters π's inputs (retrieval/pages/tool metadata), not only post-model
Q_E; B needs a side-effect ledger in S. Architectural invariants stated
(model sees only C; outputs are proposals; γ gates side effects; terminals
partitioned). Complexity/LBA material marked heuristic, not definitional.
An LLM-judge verifier is a learned kernel, not deterministic ρ.
A cold external review (same priors, no path-dependence) surfaced three real gaps
the iterative chain missed, plus precision items. Folded in:
Substantive:
- Stochastic controller: the deterministic π,ρ,H are the Dirac special case of a
controller kernel K_C(s,dc) (routing, sampled retries, ensembles, learned
routers). Deterministic is the case worth wanting (localizes randomness); the
split widens, not breaks, under stochastic control.
- Minimax type fix: the adversary chooses a POLICY/kernel, not the realized
sample. Display is now sup over α of ∫ V(ρ(s,y,e)) Q_E^α(s,y,de), not sup over
the post-probability e.
- Reach-avoid security: add a bad set B; injection steers toward B (wrong
acceptance, exfiltration, unauthorized tool use, privilege escalation,
irreversible effects), so security is reach-avoid p_ok=Pr(τ_{H_ok}<τ_B) with a
barrier certificate for B, not liveness. B and H_ok added to the tuple.
- Unconditional V*_ok is infinite under any positive pre-acceptance failure
probability ⇒ the workable object is p_ok (or the regenerative time on restart).
Precision / hygiene:
- Compiler claim scoped to a specific data-flow analysis (not a whole compiler);
add integrability/optional-stopping conditions to the hitting-time bound.
- Formal hygiene: spaces measurable, τ/τ* stopping times, H absorbing.
- Mid-generation tool calls interleave the loops — clean nesting is an
idealization needing a finer state machine.
- Soften SSM ("different", not "tighter"); demote "manifold" to informal
shorthand in the formal section; gloss "all undefined behavior" as "no complete
formal source-language semantics."
Not changed: V* incompressibility (already labeled conjectural in Grounding).
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.
The review's verdict was "mergeable"; these are its three optional items plus the
delta-attribution nit.
- δ attribution: sampled-state coverage is an evaluation-protocol property, not a
weights property. Attribute the noise floor / residual risk to the trained
weights, the environment, AND the evaluation distribution.
- reachable(L) is harness-relative too (same reason U_H(L) is): rename to
reachable_H(L) and note the divergent set D is likewise relative to H.
- Split the dense frontier paragraph in two: (1) the SR / fundamental-matrix /
potential-operator identity with its caveats; (2) the speculative interlingua/
certificate thesis. No content change.
- Grounding: add the absorbing-chain fundamental matrix (Kemeny & Snell 1960),
the general-state potential/Green operator (Revuz 1984), and Koopman (Koopman
1931; Lyapunov-from-eigenfunctions, Mauroy & Mezić 2016) to Proven; mark the
Koopman/certificate co-determination (spectral-assumption-dependent) and the
interlingua/certificate identification as Asserted.
- U(L) is harness-relative: tools and decompositions change membership, so rename
to U_H(L) and note the shell's verified tools / decompositions determine what
can be paged or outsourced.
- Countable fundamental matrix: lead with the Neumann series N=Σ Q_tr^n, scope
countable to convergence, and write (I-Q_tr)^{-1} only when the inverse exists;
general-state version is the same series read as the potential (Green) operator.
- Distinguish failure modes for V*_ok: infinite under a formal success predicate
vs undefined if no predicate has been specified.
- Soften the delta "floors" line: mu(D), sampled-coverage, and Var[tau*] drive
the empirical noise floor / residual risk, they are not literal floors of the
drift slack.
- Hedge the Koopman bridge (the last frontier thread): the eigenbasis claim
presumes a diagonalizable, point-spectrum operator — mixing dynamics carry
continuous spectrum and admit no eigenbasis — and the linearizes/certificate-
decomposes coincidence holds only for a V in the span of those eigenfunctions.
Address the round-five review's three precision points (plus the adaptive-adversary
refinement).
- Absorption is finite expected hitting time, not positive recurrence: replace
"positive-recurrent to H" with "reached in finite expected time," domain
{s : E_s[τ_H] < ∞}. Positive recurrence stays reserved for the daemon/
ready-state case (where it is used correctly).
- The fundamental matrix N=(I-Q_tr)^{-1}=Σ Q_tr^n is the finite/countable object;
the formal model lives on general measurable spaces, so add the general-state
potential (Green) operator G=Σ Q_tr^n with G·1=V* where the series converges.
Q_tr now stated as the sub-stochastic kernel restricted to H^c.
- V*_ok is taken on the process where H\H_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 restarts it. This is the
mechanism by which a U(L) task sends V*_ok → ∞.
- Adaptive adversary: nonstationary Q_{E,n} → time-ordered product; an adaptive
adversary → controlled / game-value operator (not merely time-indexed).
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.
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."
Address the three follow-up points on the first review patch.
- Reconcile the model kernel's two types: M_W(c,dy) maps into 𝒴, while the
transformer line writes M_W(c)=Law(c_τ) over contexts. Add the readout R:
𝒴 is either c_τ itself (𝒴=𝒞) or a deterministic readout R(c_τ), with
M_W(c,dy)=Law(R(c_τ)∈dy).
- Separate harness state 𝒮 from model-visible context 𝒞: the L wall binds 𝒞
(the L×d residual stream), not 𝒮. External stores (files, DBs, vector stores,
durable memory) are shell-supplied memory that extends addressable storage but
not the per-pass resident set — every read still routes through the ≤L window.
Retype U(L) accordingly: not data exceeding L (pageable) but irreducible
per-step working set exceeding L (not pageable).
- Make the time-homogeneity assumption explicit at the formal kernel: the
displayed T is the fixed-kernel case; nonstationary/adversarial environments
replace Q_E with a time-indexed kernel Q_{E,n} / admissible family, which the
minimax certificate downstream quantifies over.
Address the accepted points from an external peer review while preserving the
controller/plant thesis and the document's voice (layer, don't flatten).
- Claim: replace the ill-typed `T = ρ ∘ (M_W ∘ π, E)` with the integral
transition kernel over (𝒴,ℰ); add explicit informal/formal split; demote the
residual-stream implementation from definitional to a kept specialization
(M_W as a general learned kernel); weaken "fixpoint searches" to hitting-time
processes with fixpoint as one mode.
- Reading-it: note s is Markov only after state augmentation; mark controller
determinism as conditional on versioned code/config/endpoint/interfaces.
- The limit: rephrase "carries no descent function by construction" to "supplies
no certificate automatically" (a certificate is sufficient, not provided for
free); label V* incompressibility as conjecture, not theorem.
- δ: "measure" → "estimate"; demote empirical δ from certificate to calibrated
risk metric (confounds: bad V̂, coverage, sup not attained, nonstationarity,
non-Markov); certificate only once statistically bounded.
- Cash-out: split "soundness is free" into syntactic soundness (free) vs
semantic adequacy (empirical).
- Qualify the single-pass TC^0 claim (fixed-depth/fixed-precision; log-depth
changes it) in both body and Grounding.
- Add an operational falsification program (state-ablation, determinism audit,
drift calibration, adversarial-environment, boundary-control ablation).
Citations with a proven-vs-asserted split; the orthogonal context-length
tape bound (TC^0 single pass, the U(L) non-haltable region); and a flagged
frontier coda on V* and the semantic interlingua as one object.
A one-formula definition of a harness — a deterministic controller in
closed loop with a stochastic learned plant — and the certificate it
provably can't carry. The headline equation sits at the top of the
README and links through to the full doc.
Patrick Buckley