Paper deep dive
Verification and Self-Improvement in Agentic AI: Foundations and Limits
Chien-Ping Lu
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 90%
Last extracted: 10/9/2026, 7:36:39 AM
Summary
This paper establishes a formal framework for verifying and analyzing self-improvement in Agentic AI systems. It defines 'stages' comprising verification protocols, support interfaces, and terminal checkers to distinguish between improvements from better search, additional support, and protocol modifications. The authors introduce 'native reach' and 'closure frontier' as metrics for system capability, proving that independent majority amplification preserves these languages while existential acceptance can lead to false positives. The work places randomized-verifier classes within the polynomial hierarchy and analyzes the limits of recursive self-improvement under bounded self-modification.
Entities (7)
Relation Signals (9)
Native Reach → issubsetof → Closure Frontier
confidence 95% · LR(S)⊆FR(S)⊆dom(R)
Sigma_k^P → issubsetof → Sigma_k^RV
confidence 92% · The randomized-verifier classes satisfy ΣkP⊆ΣkRV⊆Σk+1P
Sigma_k^RV → issubsetof → Sigma_{k+1}^P
confidence 92% · The randomized-verifier classes satisfy ΣkP⊆ΣkRV⊆Σk+1P
Agentic AI → improvesvia → searching longer
confidence 90% · Agentic AI systems can improve by searching longer, receiving additional support, or modifying how they propose and verify outputs.
Agentic AI → improvesvia → receiving additional support
confidence 90% · Agentic AI systems can improve by searching longer, receiving additional support, or modifying how they propose and verify outputs.
Agentic AI → improvesvia → modifying verification protocol
confidence 90% · Agentic AI systems can improve by searching longer, receiving additional support, or modifying how they propose and verify outputs.
Majority Amplification → preserves → Native Reach
confidence 88% · We prove that independent majority amplification preserves both languages...
Majority Amplification → preserves → Closure Frontier
confidence 88% · We prove that independent majority amplification preserves both languages...
Recursive Self-Improvement → remainswithin → Verification Class
confidence 85% · For recursive self-improvement, uniformly bounded self-modification... remains within the same verification class.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Agentic AI systems can improve by searching longer, receiving additional support, or modifying how they propose and verify outputs. A performance score does not distinguish these mechanisms. We compare these changes through bounded verification with hidden terminal randomness. A stage specifies admissible transcripts, polynomial bounds, an alternating verification protocol, and a terminal checker. Its native reach uses default support; its closure frontier permits all support already admitted by the interface. Under a uniform pointwise probability gap and task-relative soundness, these are well-defined languages. We prove that independent majority amplification preserves both languages, whereas existential acceptance over random tapes can admit incorrect outputs. Exact verification is the zero-randomness case, with placement and completeness results. The randomized-verifier classes satisfy $\Sigma_k^{\mathrm{P}}\subseteq\Sigma_k^{\mathrm{RV}}\subseteq\Sigma_{k+1}^{\mathrm{P}}$; strict enlargement and depth separation require explicit complexity assumptions, while $\mathrm{BPP}=\mathrm{P}$ yields exact companions with the same frontiers. Representation analysis separates invariant acceptance from core-versus-support labels that can change under refactoring. For recursive self-improvement, uniformly bounded self-modification under a common sound interpreter and fixed verification protocol remains within the same verification class. A separate conditional-error budget controls false selection across adaptively chosen candidates. A quota-enforced XOR-synthesis family separates unbounded ratios of search success from changes in the accepted languages; exact and probabilistic audits check the resulting evidence requirements. The framework ties self-improvement claims to obligations on correctness, admissible evidence, verification resources, and selection error.
Tags
Links
- Source: https://arxiv.org/abs/2610.10611v1
- Canonical: https://arxiv.org/abs/2610.10611v1
Trouble viewing inline? Open PDF directly →
Full Text
93,440 characters extracted from source content.
Expand or collapse full text
Verification and Self-Improvement in Agentic AI: Foundations and Limits Chien-Ping Lu Abstract Agentic AI systems can improve by searching longer, receiving additional support, or modifying how they propose and verify outputs. A performance score does not distinguish these mechanisms. We compare these changes through bounded verification with hidden terminal randomness. A stage specifies admissible transcripts, polynomial bounds, an alternating verification protocol, and a terminal checker. Its native reach uses default support; its closure frontier permits all support already admitted by the interface. Under a uniform pointwise probability gap and task-relative soundness, these are well-defined languages. We prove that independent majority amplification preserves both languages, whereas existential acceptance over random tapes can admit incorrect outputs. Exact verification is the zero-randomness case, with placement and completeness results. The randomized-verifier classes satisfy Σk⊆Σk⊆Σk+1 _k P _k RV _k+1 P; strict enlargement and depth separation require explicit complexity assumptions, while = BPP= P yields exact companions with the same frontiers. Representation analysis separates invariant acceptance from core-versus-support labels that can change under refactoring. For recursive self-improvement, uniformly bounded self-modification under a common sound interpreter and fixed verification protocol remains within the same verification class. A separate conditional-error budget controls false selection across adaptively chosen candidates. A quota-enforced XOR-synthesis family separates unbounded ratios of search success from changes in the accepted languages; exact and probabilistic audits check the resulting evidence requirements. The framework ties self-improvement claims to obligations on correctness, admissible evidence, verification resources, and selection error. 1 Introduction How do changes to an agent’s search, support, and checker affect which tasks its verification protocol can accept? Consider a coding agent that proposes a patch, receives test feedback, and proposes a repair. A higher success rate can have several explanations. The same proposer may have searched for longer. Previously unavailable feedback may now expose the defect. The final checker may enforce a different correctness condition. Or the protocol may require a proposal to survive every challenge in a specified domain. These changes have different consequences even when the software diagram still contains the same three boxes: proposer, critic, and checker. The distinction becomes sharper when the checker is randomized. A correct patch may pass reliably while an incorrect patch passes occasionally. Counting any successful run as proof of capability can therefore confuse a lucky acceptance with a valid solution. Repeated evaluation can reduce a known error probability, but cannot repair a judge that is systematically wrong. We study verification procedures for which both the probability guarantee and its connection to task correctness can be stated explicitly. Our unit of analysis is a deployed stage: a fixed family of permitted verification procedures, including its interfaces and resource bounds. The task relation records which outputs count as correct. A support state supplies bounded auxiliary information, such as a test result. A transcript records a permitted interaction. The exposure relation says which transcripts the interface admits, and the core is the terminal checker. The definitions concern families indexed by input length; a single finite model checkpoint or benchmark score does not determine such a family. Two sets summarize a stage. Its native reach contains the inputs with an accepted solution under default support. Its closure frontier contains the inputs with an accepted solution under any support the current interface already permits. The word “frontier” denotes this entire set, not its topological boundary. More attempts can make an existing solution easier to find without changing either set. Making optional feedback routine can enlarge native reach within the old frontier. Admitting a previously forbidden transcript can enlarge the frontier itself. An explicit finite example in Section 7 distinguishes all three changes. Figure 1 summarizes these comparisons as sets of task inputs. The search probability is a separate quantity; it is not represented by the size of either set. (a) Better search(b) Internalization(c) Frontier expansionL′=L =LF′=F =F Higher success probability; same accepted-input sets. L′L F′=F =F L⊊L′⊆FL L F; more default access. F′F L′L x⋆x_ x⋆∈L′∖Fx_ ∈ L F; beyond the old frontier. native reachclosure frontierprevious boundary Figure 1: Three comparisons under a common task relation. Each shape represents task inputs; area is schematic and does not measure probability or cardinality. Write L=LR(S)L=L_R(S), F=FR(S)F=F_R(S) and use primes for the successor. Better search can preserve both languages. Internalization enlarges native reach within unchanged optional support. The illustrated frontier expansion admits an input natively that has no accepted source-frontier witness. This nested drawing is one possible transition, not an assumption that every stage change is monotone. The probabilistic model is the main setting. Witnesses and verification moves precede hidden terminal coins, and each complete verifier tuple has acceptance probability at most 1/31/3 or at least 2/32/3. A separate soundness requirement connects the resulting quantified acceptance rule to task correctness. These conditions include exact checkers and certified randomized algorithms. They exclude generic learned judges for which only average accuracy is known. Section 9 gives a standard randomized algebraic check that satisfies the contract, and explains why calibration alone does not establish it. Recent self-improving agents make stage comparisons concrete: code, memory, and evaluation procedures can change between accepted versions, and an improved agent can help produce its successor [12, 13, 14]. We therefore distinguish the deployed stage, the procedure that modifies it, and the rule that selects a successor. Recursion describes a feedback relation among these components; it does not by itself establish a change in verification depth or escape from a declared frontier. The autonomy roadmap of Duan et al. [1] analyzes which improvement decisions a system controls and which changes its successors inherit. Its autonomy levels are distinct from the quantifier depth studied here. We take that loop perspective as motivation and ask a complementary question: which changes preserve a declared acceptance language, and what evidence certifies a change to it? Contribution. The contribution is a semantics for three comparisons: a better search policy can preserve every admitted task input; an enforced interface change can certify coverage beyond the old frontier; and a checker refactoring can change component labels while preserving accepted behavior. Native/frontier languages, a task-soundness contract, and representation invariants make these distinctions precise. Expressive completeness supplies a representation guarantee for language pairs at each declared level. Classical complexity tools locate those languages and give conditional depth obstructions, while uniformly bounded self-modification stays within a fixed verification class. A separate conditional-error contract bounds false successor selections. An executable XOR-synthesis family exhibits arbitrarily large ratios of per-attempt success probability with identical frontiers, and frontier changes caused by an enforced bound on candidate-program references. That bound is distinct from the number of search attempts. Finite audits check the examples and their evidence requirements. The hierarchy bounds and conditional non-compilability arguments use classical complexity theory; they are not new separations of complexity classes. The semantic containment diagnostic and bounded self-modification result do not require those separation assumptions. All structural comparisons concern declared verification families. They allow better search and higher empirical success within an unchanged frontier, and do not impose a rate or ceiling on open-ended self-improvement. The paper is self-contained. Section 2 supplies the deterministic background; Section 3 defines probabilistic stages and their exact specialization. Sections 4–6 establish stability, transition diagnosis, and conditional limits. Section 7 gives executable finite examples and a declaration protocol. Section 8 applies the framework to recursive self-improvement. Related work and scope limitations close the main discussion. Appendix A contains the detailed proofs, Appendix B develops the supporting representation machinery, and Appendix C gives reproduction instructions. Appendix D compares the self-improvement mechanisms and their evaluation requirements. 2 Preliminaries: the deterministic foundation Inputs, outputs, and messages are finite binary strings under fixed encodings. Write n=|x|n=|x|. A task relation R⊆X×ZR X× Z is polynomially balanced if there is a polynomial q such that R(x,z)⇒|z|≤q(|x|)R(x,z) |z|≤ q(|x|). This bounds every valid encoded output. It does not assert that R is decidable in polynomial time, or that a valid output can be efficiently found. For a bounded patching task, x contains the program and specification, and z is a patch of the declared maximum length. Certificates and alternating verification (classical background). P is deterministic polynomial time. A language is in NP if membership has a polynomial-length certificate checked in polynomial time. More generally, for fixed k≥1k≥ 1, write ky→=∃y1∀y2∃y3⋯Qkyk,Q_k y=∃ y_1\,∀ y_2\,∃ y_3·s Q_ky_k, with each string ranging over a nonempty polynomially bounded domain. A language L is in Σk _k P when x∈Lx∈ L is equivalent to ky→V(x,y→)=1Q_k y\,V(x, y)=1 for a deterministic polynomial-time predicate V. The universal-start version defines Πk _k P, and =⋃k≥0Σk PH= _k≥ 0 _k P with Σ0= _0 P= P. These are standard bounded-alternation characterizations [2]. There are k quantifier blocks and k−1k-1 switches between quantifier types; “depth” below counts blocks. For example, ∃a∀u∃vV(x,a,u,v)∃ a\,∀ u\,∃ v\,V(x,a,u,v) says that some proposal a has a valid reply v for every challenge u. The reply may depend on u, while a cannot. A sampled critic does not implement ∀u∀ u. An exhaustive search over the bounded domain, or a separately justified certificate for the same universal condition, is needed. A polynomial bound on the length of u permits exponentially many challenges. Thus a polynomial-time terminal predicate does not make the whole quantified game a polynomial-time executable agent. Existential start matches proposal-first verification. Challenge-first games have the universal-start dual. Several proposals without an intervening universal block can be concatenated into one existential string if the total length remains polynomial. This is the formal reason that additional sampled reasoning traces need not increase depth. Randomized terminal predicates. BPP consists of languages decidable in polynomial time with two-sided error at most 1/31/3 on every input. We use it for a tuple-level predicate, after the verification moves have been specified. The classical containment ⊆Σ2∩Π2 BPP _2 P∩ _2 P is the Sipser–Gács–Lautemann bound [3, 4]. These background facts will locate the stage languages. They do not identify the stage declaration of an observed product. 3 Probabilistic stages and exact specialization Definition 3.1 (Bounded probabilistic stage). A stage for a polynomially balanced task R is S=(k,pS,σ0,ExpS,CoreS)S=(k,p_S, _0,Exp_S,Core_S), with the following data and contracts. (i) k≥1k≥ 1 is fixed. The polynomial pS(n)p_S(n) bounds the lengths of support σ, transcript t, output z, and each verification move yiy_i. Each object type has its own declared polynomial length limit within this common envelope. Raising the envelope to encode a longer transcript does not expand the other domains. A move ranges over all binary strings up to its declared limit. The default support σ0(x) _0(x) is uniformly polynomial-time computable and admissible; we suppress its input argument when unambiguous. All quantified domains include the empty string. (i) ExpS(x,σ,t)Exp_S(x,σ,t) is a deterministic polynomial-time predicate that checks admissible support and transcript encodings and their length bounds. Support supplies data through this interface; it does not install an oracle. (i) CoreS(x,z,t,y→,r)Core_S(x,z,t, y;r) is a uniform polynomial-time Boolean predicate. Here r is uniform on 0,1ρS(n)\0,1\ _S(n) for a declared polynomial ρS _S. Its runtime has a polynomial bound separate from the object-length bound. Malformed encodings are rejected. The random tape is hidden until after all moves, so moves cannot depend on it. (iv) On every well-formed bounded tuple w=(x,z,t,y→)w=(x,z,t, y), the acceptance probability obeys aS(w):=Prr[CoreS(w;r)=1]∈[0,1/3]∪[2/3,1].a_S(w):= _r[Core_S(w;r)=1]∈[0,1/3]∪[2/3,1]. (1) Define DS(w)=aS(w)≥2/3D_S(w)=1\a_S(w)≥ 2/3\, with value zero on malformed or out-of-bound tuples, and define quantified acceptance S(x,z,t)⟺ky→DS(x,z,t,y→)=1.A_S(x,z,t) _k y\ D_S(x,z,t, y)=1. (2) (v) Task-relative soundness holds: for every exposed transcript, ExpS(x,σ,t)∧S(x,z,t)⟹R(x,z).Exp_S(x,σ,t)\ \ A_S(x,z,t) R(x,z). (3) The coin and runtime bounds are part of the core specification. Increasing them alone does not increase the domains of support, output, or moves. The tuple retains the exact stage interface while allowing hidden core coins. The gap makes DSD_S a total BPP predicate on encoded tuples: the original randomized algorithm decides its high-probability set. This observation requires the gap on all bounded tuples, with an efficiently checked encoding domain. A promise on an unspecified, computationally inaccessible subset would not justify the same BPP or derandomization claims. What soundness requires. The gap and soundness are different assumptions. A checker that confidently accepts a false answer can satisfy the gap and violate soundness. Conversely, at depth two a false output can have a locally accepting move and still be rejected by the quantified game: D(a,u)=u=0D(a,u)=1\u=0\ satisfies the gap, but ∃a∀uD(a,u)∃ a\,∀ u\,D(a,u) is false on the Boolean challenge domain. Thus quantified soundness is not equivalent to requiring low acceptance on every move tuple of every false output. The latter is sufficient and stronger. At depth one it is equivalent on exposed transcripts. In a patch audit, σ can encode a counterexample, t the bounded proposal/test/repair record, and the final z the patch to certify. Any verification moves after z support or challenge that fixed patch. If the output itself must change in response to a universal challenge, a different game with an output strategy is required; it is not silently encoded as a fixed output in (2). Input and support x,σx,σ Admissible record ExpS(x,σ,t)Exp_S(x,σ,t) Output and moves z,ky→z,Q_k y Terminal checker CoreS(w,r)Core_S(w;r) Hidden coins r Figure 2: The declared verification interface. Exposure and length bounds fix the admissible records; alternating moves specify the acceptance game. Only the terminal checker receives hidden random bits. Setting the coin length to zero recovers deterministic verification. The diagram specifies semantics, not the cost of solving the quantified game. Definition 3.2 (Native reach and closure frontier). Let NatS(x)=t:ExpS(x,σ0,t),ExpS∗(x)=t:∃σExpS(x,σ,t).Nat_S(x)=\t:Exp_S(x, _0,t)\, _S^*(x)=\t:∃σ\ Exp_S(x,σ,t)\. All objects are bounded as in Definition 3.1. Define LR(S) _R(S) =x:∃t∈NatS(x)∃zS(x,z,t), =\x:∃ t _S(x)\ ∃ z\ A_S(x,z,t)\, (4) FR(S) _R(S) =x:∃t∈ExpS∗(x)∃zS(x,z,t). =\x:∃ t _S^*(x)\ ∃ z\ A_S(x,z,t)\. (5) These symbols use bounded-error acceptance throughout; the superscript exex will denote an exact specialization when comparison is needed. For a concrete instance, let x=(1d,a)x=(1^d,a) specify a Boolean linear function, and let t=zt=z list its referenced variables. Optional support selects a quota q≤B(d)q≤ B(d), defaulting to b0(d)b_0(d). Exposure requires |t|≤q|t|≤ q; an exact coefficient check establishes correctness. Native reach then requires ‖a‖0≤b0(d)\|a\|_0≤ b_0(d), and the frontier requires ‖a‖0≤B(d)\|a\|_0≤ B(d). Section 7.3 specifies and proves this instance. These are languages of task inputs, not sets of accepted patches or measures of success probability. Existence of an accepted witness is weaker than efficient production of that witness by a given learned policy. A support source must be bounded and its admissibility polynomially checkable under the declared interface. A fact supplied by an unmodeled oracle cannot be called conservative merely because it fits in a short string. Definition 3.3 (Randomized-verifier classes). For k≥1k≥ 1, a language L belongs to Σk _k RV if some polynomial-time randomized predicate V(x,y→,r)V(x, y;r) has a pointwise gap on all bounded tuples and x∈L⟺ky→[Prr(V(x,y→;r)=1)≥2/3].x∈ L _k y\ [ _r(V(x, y;r)=1)≥ 2/3]. Πk _k RV is the universal-start dual. On no-instances the gap gives the dual quantifier formula with threshold at most 1/31/3 by negation. This is a paper-specific notation for bounded alternation over a total BPP predicate. At depth one, ⊆Σ1⊆ NP _1 RV MA: the witness is chosen before the coins. The additional pointwise restriction applies even to losing witnesses on yes-instances, so equality with standard MA is not assumed. Placing the probability outside the existential witness instead gives public-coin semantics; it changes the information available to the witness and must be modeled separately [5]. Proposition 3.4 (Placement and deterministic recovery). For a sound stage of depth k, LR(S)⊆FR(S)⊆dom(R),LR(S),FR(S)∈Σk.L_R(S) _R(S) (R), _R(S),F_R(S)∈ _k RV. An exact stage has ρS=0 _S=0, hence DS=CoreSD_S=Core_S. Its native and frontier languages belong to Σk _k P, and its exact and probabilistic readings coincide. Permitted support can be selected with the first existential move; exact checking removes only the terminal randomness. The proof is in Appendix A.1. Theorem 3.5 (Expressive completeness of native/frontier pairs). Fix k≥1k≥ 1 and L0⊆L1L_0 L_1 with both languages in Σk _k RV. There is a sound depth-k stage with LR(S)=L0L_R(S)=L_0 and FR(S)=L1F_R(S)=L_1 for a polynomially balanced task R. If both languages are in Σk _k P, the stage can be exact. The proof is in Appendix A.1. This is a representation theorem: the interface loses no pair of languages in the declared class. It is not a procedure for learning a verifier or discovering the exposure sets of a product. Together with Proposition 3.4, it supplies the deterministic foundation without reliance on a separate paper. 4 What randomization changes 4.1 False acceptance and amplification Proposition 4.1 (Existential coins can create false frontier membership). There is a sound depth-one stage for which replacing bounded-error acceptance by ∃rCoreS=1∃ r\,Core_S=1 strictly enlarges the frontier and accepts inputs outside the task domain. A false answer can have a rare accepting tape while remaining below the bounded-error threshold. The proof is in Appendix A.2. The pathology changes the acceptance semantics, not the stage. It justifies keeping verifier randomness outside the control of witnesses and measuring bounded error rather than treating one success as a certificate. Theorem 4.2 (Amplification preserves the frontier). Fix a stage S and a polynomial-time computable, odd positive, polynomially bounded repetition count N(n)N(n). Replace its terminal core by a strict majority of N(n)N(n) independent runs on the same tuple. Preserve all object and move domains and the exposure relation, while allowing polynomially more coins and runtime. The resulting stage S[N]S^[N] has the same DSD_S, quantified acceptance, native reach, and frontier. Its pointwise error is at most e−N/18e^-N/18. Independent majority improves reliability without moving any tuple across the acceptance gap. The proof is in Appendix A.2. For any constant 0<δ<1/20<δ<1/2, sufficiently many odd repetitions yield error at most δ with the same acceptance language, using threshold 1−δ1-δ for the amplified predicate. The runtime and raw core implementation change, but semantic authority does not. Preserving the witness domains is essential: enlarging them while amplifying would be a separate stage change. Repeatedly sampling different candidate answers is a search policy, not the verifier amplification covered by this theorem. Correlated judge calls also do not satisfy its independence premise. Figure 3 shows how the majority rule preserves the gap and why accepting any successful repetition has a different effect. 001/31/32/32/311001/31/32/32/311excludedgapSingle-call acceptance ppMajority acceptance(a) Majority responseN=1N=1N=3N=3N=15N=15115599131317172121000.250.250.50.50.750.751137/6437/645/325/32Independent calls N (odd)False-acceptance probability(b) False acceptance at p=1/4p=1/4Any passMajority Figure 3: Reliability depends on the aggregation rule. (a) The exact binomial majority map gN(p)g_N(p) sends each admissible low-probability tuple to the low side and each high-probability tuple to the high side. The shaded open interval is excluded by the pointwise gap. Preserving this classification preserves quantified acceptance and the two languages (Theorem 4.2). (b) For the same fixed false tuple with single-call probability 1/41/4, independent majority reduces false acceptance, whereas “any pass” gives 1−(3/4)N1-(3/4)^N. At three calls these are 5/325/32 and 37/6437/64. Curves are analytic, with the tuple and exposure held fixed. 4.2 Classical placement and conditional comparisons Theorem 4.3 (Sandwich bound). For every k≥1k≥ 1, Σk⊆Σk⊆Σk+1,Πk⊆Πk⊆Πk+1. _k P _k RV _k+1 P, _k P _k RV _k+1 P. Replacing the terminal randomized predicate by its classical alternating representation costs at most one extra block. The proof is in Appendix A.3. The bound concerns families of expressible languages. It does not assign an “exact frontier” to an arbitrary randomized stage by changing a label. No general nested-ring comparison of exact and randomized frontiers of the same physical checker follows from it. Theorem 4.4 (Conditional enlargement and derandomization). (i) If Σ1⊈ _1 RV NP, some sound randomized depth-one stage has a frontier that no exact depth-one stage can equal. (i) If = BPP= P, then Σk=Σk _k RV= _k P and Πk=Πk _k RV= _k P for all k. Every randomized stage has a sound exact companion with the same depth, object domains, exposure, native reach, and frontier, allowing a different polynomial bound on terminal runtime. The proof is in Appendix A.3. The enlargement premise is specific to the pointwise-gap class; ≠ MA≠ NP alone does not supply it. Failure of = BPP= P would not by itself prove strict stage-frontier enlargement either. These are conditional comparisons, not demonstrated advantages of a deployed neural judge. 5 Representation invariants and structural diagnosis Define the transcript-indexed accepted-input set KS(x,t)⇔∃zS(x,z,t)K_S(x,t) ∃ z\,A_S(x,z,t). A comparison uses a fixed common transcript encoding, including rejection outside the declared domains. When encodings differ, an explicit translation is required. Definition 5.1 (Semantic authority). Write T⪯authST authS if KT(x,t)⇒KS(x,t)K_T(x,t) K_S(x,t) for all x,tx,t. This compares quantified acceptance, possibly across different depths. Authority here is acceptance of task inputs per transcript; it is not raw model accuracy, nor necessarily containment of every accepted output. Both stages must be sound for the same task. Opposite inclusions define equivalence. A comparison should also survive changes of encoding. Polynomial transcript translations and a representation using just default and optional support preserve the two languages under the conditions developed in Appendix B.1. Proposition 5.2 (Guard transfer). For a deterministic polynomial-time guard g(x,t)g(x,t), the stages (ExpS∧g,CoreS)and(ExpS,g∧CoreS)(Exp_S g,Core_S) and (Exp_S,g _S) have the same native reach and frontier, with all other data fixed. A guard can reject the same records at either interface without changing accepted behavior. Appendix A.4 proves the result; Appendix B.2 characterizes the associated local invariant. This invariance explains an audit limitation. With one input and two transcripts a,ba,b, let a source expose and accept only a. A target that exposes only a and whose core accepts both transcripts has a raw authority change. Moving the guard for a into the target core produces an equivalent target that exposes both transcripts but accepts only a; now the raw change is exposure. Neither transition escapes the source frontier. Component labels are representation-dependent even when accepted behavior is unchanged. Theorem 5.3 (Semantic containment and escape diagnostic). If T⪯authST authS and NatT(x)⊆ExpS∗(x)Nat_T(x) _S^*(x) for every x, then LR(T)⊆FR(S)L_R(T) _R(S), regardless of their depths. More precisely, if x∈LR(T)∖FR(S)x _R(T) _R(S), every accepted target-native transcript t for that input satisfies t∉ExpS∗(x)or¬KS(x,t).t _S^*(x) or K_S(x,t). Proof. An accepted target-native t that also lies in ExpS∗(x)Exp_S^*(x) and satisfies KS(x,t)K_S(x,t) would witness x∈FR(S)x _R(S), a contradiction. Under both containment premises such a witness exists for every x∈LR(T)x _R(T). ∎ This is an elementary semantic diagnostic. It says exactly what an escape witness must violate; it does not recover those premises from benchmark scores. In particular, authority-preserving internalization of permitted support can increase native reach only within the old frontier. The familiar three-field report—depth, authority, exposure—records a useful architecture description, but is not a theorem that three causes are independent. Because authority already compares fully quantified acceptance, increased depth cannot produce escape while both semantic containment premises hold. Depth obstructions need the additional class argument of Section 6. Either core change or exposure change can realize frontier escape at fixed depth, for exact and randomized stages. Appendix B.3 gives separate constructions that keep the other component fixed. Strict escape is stronger than a changed component identifier or a failed global containment test: the latter can occur on an input that another source transcript already solves. Appendix B.4 extends the construction to finite chains. 6 Depth limits and certificate substitution Theorem 6.1 (Conditional depth obstructions). Fix k≥1k≥ 1. (i) If Σk≠Σk+1 _k P≠ _k+1 P, there is a task R and an exact depth-(k+1)(k+1) stage T whose native language is not contained in the frontier of any sound exact depth-k stage for R. (i) The analogous assertion holds for randomized depths k,k+1k,k+1 if Σk≠Σk+1 _k RV≠ _k+1 RV. (i) If Σk+1≠Σk+2 _k+1 P≠ _k+2 P, some exact depth-(k+2)(k+2) target cannot be covered by any sound randomized depth-k stage for its task. The proof is in Appendix A.5. Soundness is essential to the obstruction: a language outside a class can be a subset of a language inside that class. Nonmembership alone would not rule out coverage. Nor does this theorem say that every extra block improves every stage. Its targets are chosen separator families. Iterating it supplies different tasks at successive levels, not a training trajectory on one fixed benchmark. Under the stated assumptions, randomization at depth k cannot uniformly replace all exact depth-(k+2)(k+2) protocols. The theorem does not establish a sharp adjacent-level bound. Proposition 6.2 (When certificates can replace challenge). Let V(x,a,u)V(x,a,u) be polynomial-time with bounded strings a,ua,u, and let G(x,a)G(x,a) be a deterministic polynomial-time guard for the supported family. Suppose a polynomial-time exact checker C(x,a,π)C(x,a,π) has polynomially bounded certificates and, for every bounded (x,a)(x,a) with G(x,a)=1G(x,a)=1, satisfies ∃πC(x,a,π)=1⟺∀uV(x,a,u)=1.∃π\ C(x,a,π)=1 ∀ u\ V(x,a,u)=1. Then the guarded language x:∃a[G(x,a)∧∀uV(x,a,u)=1] \x:∃ a\ [G(x,a) ∀ u\ V(x,a,u)=1]\ =x:∃a,π[G(x,a)∧C(x,a,π)=1] =\x:∃ a,π\ [G(x,a) C(x,a,π)=1]\ has an exact depth-one certificate representation. Soundness of C alone gives containment, not equality. If this guarded language is Σ2 _2 P-complete, such a uniform sound-and-complete certificate system implies Σ2= _2 P= NP. The proof is in Appendix A.5. This is a design constraint derived from classical complexity, with two separate engineering obligations: soundness of the checker and existence of short certificates for every accepted proposal. Restricted families can satisfy both. For example, equality of two XOR circuits can be checked by computing their coefficient vectors over 2F_2, even though direct universal testing ranges over exponentially many Boolean inputs. Such a symbolic checker changes the terminal implementation and can remove explicit challenge on that family. Sampled criticism alone supplies neither obligation. 7 A reproducible audit, from exact to probabilistic 7.1 Running task and three exact designs Let x⋆x_ be the task of repairing a lookup function on the three-element array (alpha,beta,gamma)( alpha, beta, gamma). The declared input domain for testing is I=−3,−2,−1,0,1,2,3,4I=\-3,-2,-1,0,1,2,3,4\. Correct behavior returns the indexed element for 0≤i<30≤ i<3 and a default value otherwise. The candidate set contains the original buggy program, an upper-bound-only repair, and a full lower-and-upper-bound repair. The task relation is R(x⋆,z)⇔∀i∈I,z(i)=spec(i).R(x_ ,z) ∀ i∈ I, z(i)=spec(i). This example is finite and completely enumerated. It does not establish a complexity separation for general program repair. The sampled critic checks only 0,2,3,4\0,2,3,4\. The upper-bound-only repair passes all four, but at i=−1i=-1 returns gamma rather than the default. The exhaustive design checks all eight inputs. The certificate design checks a complete table of outcomes against both the candidate execution and the specification, bound to the declared task and candidate. Both exact designs reject the incomplete patch and accept the full repair. The sampled checker is deterministic as a program, but is not sound for R: deterministic testing does not imply exact verification of a broader specification. Terminal rule Incomplete patch Full repair Sound for R Four declared tests Accept Accept No All eight declared inputs Reject Accept Yes Task-bound complete certificate Reject Accept Yes Table 1: Exact enumeration on the bounded lookup task. Acceptance is relative to the declared specification and domain. The sampled design’s apparent reach cannot be used as a sound frontier for this task. The existing executable declaration includes default and optional certificate transcripts. Default support in the certificate stage supplies no valid certificate, while permitted optional support exposes the complete correct record. It therefore has LR(Scert)=∅,FR(Scert)=x⋆.L_R(S_ cert)= , _R(S_ cert)=\x_ \. The exhaustive stage exposes the valid repair natively and has both languages equal to x⋆\x_ \. These are sets of the single task input; the accepted patch projection, reported separately by the artifact, contains only the full repair. They must not be confused with one another. To isolate exposure changes, keep the certificate core fixed and compare three declarations. S0S_0 permits only the default uncertified record under all support states, so both languages are empty. S1S_1 admits the valid certificate through optional support, so native reach is empty and the frontier is x⋆\x_ \. S2S_2 makes that record native, so both languages are x⋆\x_ \. Thus S0→S1S_0→ S_1 expands support and the frontier, and S1→S2S_1→ S_2 internalizes already permitted support. The direct S0→S2S_0→ S_2 comparison exhibits native escape under unchanged authority. Repeating default attempts in S1S_1 cannot introduce the excluded native record; searching its optional support can find a record already in its frontier. This is the finite distinction between search effort, support expansion, and internalization. 7.2 A controlled stochastic extension For the same finite checker C, reject malformed and out-of-bound records deterministically. On well-formed bounded tuples, define a noisy terminal core that uses two fair bits: with probability 3/43/4 it returns C and with probability 1/41/4 it returns 1−C1-C. Accepted exact tuples now have probability 3/43/4 and rejected tuples probability 1/41/4. The gap holds, D=CD=C, and soundness and every native/frontier set are unchanged. Three independent evaluations with majority change these probabilities to 27/3227/32 and 5/325/32 without changing the sets. Existential acceptance over the two-bit tape accepts every such tuple, including the incomplete patch. This deliberately controlled example verifies the semantic distinction using exact rational arithmetic; it is not an empirical model of a learned judge. It can also expose misleading error reductions. Accepting if any of three calls accepts gives a false acceptance probability 1−(3/4)3=37/641-(3/4)^3=37/64, which violates the gap on a false tuple. The majority rule, independence, and fixed candidate are therefore substantive assumptions. 7.3 A growing family with an enforced interface Consider synthesizing a straight-line XOR program for fa(u)=⨁j=1dajujf_a(u)= _j=1^da_ju_j, given x=(1d,a)x=(1^d,a) with a∈2da _2^d. A candidate is a sorted list z of distinct variable indices and computes fz(u)=⨁j∈zujf_z(u)= _j∈ zu_j; the empty list returns zero. Correctness means fz(u)=fa(u)f_z(u)=f_a(u) for every u∈2du _2^d. The exact core compares coefficient vectors and binds the output to the program recorded in the transcript t. It rejects malformed, duplicate, out-of-range, and mismatched records. This discharges the universal condition in polynomial time on this restricted language. The harness enforces a maximum number of referenced variables. Here support selects a quota permission, rather than supplying unknown task information. It is an integer quota q∈0,…,B(d)q∈\0,…,B(d)\, defaulting to b0(d)b_0(d), and ExpB,b0(x,q,t)⇔0≤q≤B(d),t is a canonical program,|t|≤q.Exp_B,b_0(x,q,t) 0≤ q≤ B(d), t is a canonical program, |t|≤ q. Here |t||t| counts references; its binary encoding has length O(dlogd)O(d d). Assume 0≤b0(d)≤B(d)≤d0≤ b_0(d)≤ B(d)≤ d, with both quotas polynomial-time computable. The executable harness checks exposure before invoking the same core in every configuration. One ignored existential move gives depth one. Proposition 7.1 (Search gains and an enforced quota). For this uniform exact family, LR(SB,b0)=(1d,a):‖a‖0≤b0(d),FR(SB,b0)=(1d,a):‖a‖0≤B(d).L_R(S_B,b_0)=\(1^d,a):\|a\|_0≤ b_0(d)\, _R(S_B,b_0)=\(1^d,a):\|a\|_0≤ B(d)\. Two proposal policies with full support on the same candidate programs can have an unbounded ratio of per-attempt success probabilities while preserving these languages: for every target/quota pair with ‖a‖0≤q≤B(d)\|a\|_0≤ q≤ B(d), the ratio is 2d−1+1/22^d-1+1/2. If q<‖a‖0q<\|a\|_0, both probabilities are zero. For b=⌊d/2⌋b= d/2 , changing (B,b0)(B,b_0) from (b,0)(b,0) to (b,b)(b,b) internalizes support. Changing it to (b+1,b+1)(b+1,b+1) then yields native escape at every d≥1d≥ 1, witnessed by any a of weight b+1b+1. The proof, including exclusion of all old witnesses, is in Appendix A.7. An existential accepted-input language does not record the probability of finding its witnesses. For the policy comparison, a uniform d-bit mask proposes each program with probability 2−d2^-d. A second policy uses the directly computed correct program with probability 1/21/2 and that uniform proposal otherwise. At a quota admitting the correct program, their per-attempt success probabilities are 2−d2^-d and 1/2+2−(d+1)1/2+2^-(d+1). Both retain full proposal support; disallowed proposals are rejected by the harness. For M independent attempts with per-attempt success p, success is 1−(1−p)M1-(1-p)^M. This comparison charges the same attempt count and both policies are polynomial-time, but it is a controlled analytic example, not a learned improvement or a wall-clock speedup measurement. The supplied target vector already determines the correct program, so this example tests comparison semantics rather than discovery hardness. The family makes two audit decisions concrete. Raising the number of attempts changes discovery probability. Raising an enforced quota changes admissible programs and can change the frontier even though every language here is in P. A budget that is only advisory supplies no such exclusion proof. The reference implementation enumerates all target vectors, candidate programs, and quotas for 1≤d≤61≤ d≤ 6, tests malformed and forged records, and checks the formulas using exact arithmetic. At d=6d=6, the three configurations above have (|L|,|F|)(|L|,|F|) equal to (1,42)(1,42), (42,42)(42,42), and (57,57)(57,57). The general statement follows from the proof, not extrapolation from these finite counts. Figure 4 displays these exact finite sets alongside the policy comparison at a fixed permitted quota. The two panels measure different objects even though they use the same task family. (a) Admitted task inputs at d=6d=6Target weight ‖a‖0\|a\|_0(|L|,|F|)(|L|,|F|)00112233445566 Source (B,b0)=(3,0)(B,b_0)=(3,0) (1,42)(1,42)NOOO– Internalized (B,b0)=(3,3)(B,b_0)=(3,3) (42,42)(42,42)N– Expanded (B,b0)=(4,4)(B,b_0)=(4,4) (57,57)(57,57)N–Number oftargets1615201561N: native O: optional only –: blocked 1248163264000.250.250.50.50.750.7511Proposal attempts MMAt least one success (b) Search with the same quota Uniform: p=1/64p=1/64Mixture: p=65/128p=65/128 Figure 4: Enforced permission and discovery probability in the XOR family. (a) Each column represents all target vectors of one Hamming weight, with multiplicities shown below. Making quota three the default changes native reach from one to 42 inputs without changing the frontier. Raising the maximum quota to four also admits the 15 weight-four targets. (b) Both policies use the source stage with explicit optional quota q=3q=3 and target a=(1,1,1,0,0,0)a=(1,1,1,0,0,0); under default quota zero both have success probability zero. For M independent attempts the curves are 1−(1−p)M1-(1-p)^M. The solution mixture computes the correct program with probability 1/21/2 and samples uniformly otherwise; it is an analytic control, not a learned RSI system. Counts and per-attempt probabilities match the exact audit of Proposition 7.1. This example proves Proposition 7.1 uniformly and audits its finite instances; the policy probabilities are analytic quantities. It does not instantiate an adaptive learned improver. The uniform-envelope result in Proposition 8.1 and the conditional selection bound in Proposition 8.2 are separate theorems with separate premises. 7.4 Declaration protocol and disagreement rules A reproducible audit first records the following evidence, before assigning complexity labels or claiming an escape. 1. Task and encoding. Specify input size, output meaning, the correctness relation, and any restricted domain. Separate test-suite correctness from full program correctness. 2. Stage and budgets. Version the model, decoder, interface, default support, optional support, transcript grammar, object-length bounds, coin policy, and runtime bounds. Trace permissibility needs an executable predicate or a proof; one observed trace establishes only one possibility. 3. Acceptance contract. Identify the final checker and provide task-soundness evidence. A randomized checker additionally needs a uniform gap argument. Average agreement is insufficient. Universal moves need exhaustive bounded semantics or an equivalent proved procedure. 4. Comparison. Align task and transcript encodings. Prove authority/exposure containment, or exhibit a counterexample to it. A frontier escape claim additionally needs an accepted target input and evidence excluding all source-frontier witnesses for that input. 5. Audit status. Record established conclusions relative to validated premises, candidate claims awaiting specific evidence, and indeterminate claims with missing or disputed premises. Preserve competing declarations rather than voting one into truth. A schema linter can reproduce the consequences of identical evidence records. It cannot validate an arbitrary semantic inclusion from a certificate string or make two auditors agree about an opaque deployment. A false output proved to satisfy SA_S on an exposed transcript falsifies task soundness. One observed false stochastic acceptance does not: it may be a permitted low-probability event. At depth greater than one, locally high acceptance also need not imply quantified acceptance. A proved admissible tuple with probability in (1/3,2/3)(1/3,2/3) falsifies the gap; a supposedly universal critic that checks only a sample invalidates that depth declaration. Finite measurements can reveal counterexamples but do not in general prove uniform contracts on an infinite family. An unobserved trace is not evidence that it is forbidden. The patching artifact supplies a content-addressed declaration, exact outcomes, accepted input languages, and separate output projections. The additional probabilistic artifact enumerates random tapes and uses rational probabilities. The patching artifact also distinguishes inclusion of visible facts from inclusion of actual transcripts: exhaustive-test facts can be contained in certificate-stage facts even though their encoded transcript sets are disjoint. Only the latter sets, or a proved translation between them, enter Theorem 5.3. Appendix C specifies how to reproduce the artifacts. We do not use the names of commercial systems or multiagent roles to assign established Σk _k P or Σk _k RV membership to their implementations. 8 Recursive self-improvement: agent changes and selection The framework separates two questions about self-improvement: how a successor changes the tasks its protocol accepts, and how reliably the selection process identifies an improvement. The first concerns verification structure; the second requires a separate error contract for the improvement criterion. Duan et al. distinguish structural recursion, where an inherited revision controls a later improvement round, from effective recursion, where it produces better successors under comparable budgets and independent assessment [1]. Both can occur within one verification class. Our comparison concerns the accepted languages and contracts of those successive systems; it does not replace the empirical test of improvement effectiveness. 8.1 What recent systems make observable Self-improvement can change an answer within one task, a reusable agent component across tasks, or the mechanism that generates subsequent changes. These are different comparison scopes. GEPA evolves prompts from execution feedback, ACE maintains structured contextual playbooks, and AFlow searches code-represented workflows [21, 23, 22]. RSIAgent accumulates memory without parameter updates and freezes it for subsequent evaluation [14]. Such mechanisms motivate explicit support and transcript declarations, including what the old interface already permitted. Executable components can also evolve. DGM searches an archive of modified agent programs; AHE connects harness edits to component-level observations; Self-Harness uses failure analysis and regression testing to select harness changes [12, 20, 26]. At the meta level, STOP applies a program improver to its own code while leaving the underlying language model unchanged, and Hyperagents makes both the task agent and meta agent editable [18, 19]. AIDE2 reports successive research-agent improvements and held-out transfer, while noting that its outer improver’s advantage over a strong baseline is not decisively resolved [13]. These reports make it necessary to record which component changes and which evaluation remains fixed. They provide empirical evidence within their experimental settings, rather than stage-contract or hierarchy-separation proofs. Appendix D compares the mechanisms and the evidence needed to connect them to the present model. The comparison includes the September 22 version of the RSI survey [1]. 8.2 Deployed stage, improver, and selection rule Write a proposed transition as S^i+1=Ui(Si,hi,ηi),Si+1=Ji(Si,S^i+1,hi), S_i+1=U_i(S_i,h_i; _i), S_i+1=J_i(S_i, S_i+1,h_i), where UiU_i is an improver, hih_i is its bounded interaction history, ηi _i is its proposal randomness, and JiJ_i is the selection rule. The rule can retain the old stage. A recursive loop lets an accepted change affect a subsequent improver or its inputs. It need not add a universal verification block. The task relation R used to evaluate deployed outputs must also be distinguished from the improvement criterion used by JiJ_i. A higher benchmark score is neither a proof of LR(Si)⊆LR(Si+1)L_R(S_i) _R(S_i+1) nor an escape witness. Figure 5 separates the update loop from the two contracts used to analyze it: accepted-language structure and false-selection risk. Deployed SiS_i Improver UiU_i Candidate S^i+1 S_i+1 Selection JiJ_i Next deployed Si+1S_i+1 history hih_i,proposal coins ηi _iselect candidateor retain SiS_iAccepted changes can affect later improvement rounds Structural contract Jointly uniform A,E,CA,E,C; common bounds and k Lenv∈ΣkL_ env∈ _k RV Gap and task soundness for every admitted candidate Selection contract Pr(Bi∣ℋi−1)≤δi (B_i _i-1)≤ _i Pr(⋃i=1MBi)≤∑i=1Mδi ( _i=1^MB_i)≤ _i=1^M _i Conditional validity for every selection call Count every selection call, including rejections Figure 5: An RSI loop and two distinct guarantees. The dashed feedback indicates that an accepted revision can alter later improvement, including the improver’s inputs or inherited mechanism. It does not add a quantifier block. Under Proposition 8.1’s fixed admission, exposure, interpretation, and common bounds, admitted histories define a language in the same verification class. Proposition 8.2 separately controls false selection relative to an improvement criterion. Neither guarantee alone establishes that successors are empirically better. Changes to weights, prompts, tools, or memory identify candidate stage changes; their semantic effect depends on the declared interface. A better proposal policy within an unchanged admissible transcript family can improve observed performance without changing the frontier. An added tool can change exposure or the terminal predicate. Internalizing previously optional memory can enlarge native reach inside an unchanged frontier. None of these effects is determined by the word “recursive.” Uniform complexity claims further require a uniformly described family as input size grows; unrelated checkpoints at each size must not silently supply nonuniform advice. Proposition 8.1 (Bounded self-modification inside a fixed envelope). Let h,ch,c be polynomially bounded history and candidate strings. Assume one deterministic polynomial-time admission predicate A(x,h,c)A(x,h,c), one such exposure predicate E(x,h,c,σ,t)E(x,h,c,σ,t), and one uniform polynomial-time randomized terminal interpreter C(x,h,c,z,t,y→,r)C(x,h,c,z,t, y;r). These algorithms include all encoding and object-domain checks. There are common polynomial object, coin, and runtime bounds and the same fixed k move blocks, whose domains are identical for every candidate. The default support is uniformly polynomial-time computable from (x,h,c)(x,h,c). Every admitted candidate Sh,cS_h,c satisfies the pointwise gap and quantified soundness for a common R. Choose h,ch,c before the moves and hidden coins. Then Lenv=x:∃h,c[A(x,h,c)∧x∈FR(Sh,c)]∈Σk.L_ env=\x:∃ h,c\ [A(x,h,c) x _R(S_h,c)]\∈ _k RV. The same holds with native reach in place of the frontier. With exact terminal checks both languages belong to Σk _k P. A bounded candidate program and history fit within the first existential choice when the verification interface is fixed. The proof is in Appendix A.6. This is a closure observation under explicit uniform bounds, not a claim that arbitrary self-modifying software has a sound admission test. Establishing the gap and soundness for every permitted candidate is an additional proof obligation; a syntax check alone does not establish it. The proposition also concerns existence of an accepted history, not the probability or cost of discovering it. A successor can escape the particular deployed SiS_i while remaining within this larger, fixed enclosing stage. Conversely, a run that changes the envelope, interpreter, or quantifier protocol requires a new declaration. Polynomial time for each separately fixed candidate is insufficient: the admission, exposure, and interpretation must be jointly uniform in its code. The admitted envelope can contain histories the actual improver never discovers. The result does not cover an unbounded improvement process with no common resource bound. Table 2 applies these obligations to the XOR family. Here exposure is what the harness permits. A policy need not realize every permitted record. If a different declaration instead defines exposure through policy-attainable records, policy support becomes part of that declaration and must be compared explicitly. Permitted edit Effect in the XOR family Contract to retain or establish Full-support proposal policy Changes discovery probability; L,FL,F unchanged Same exposure, output binding, and exact core. Default quota 0→b0→ b Sets L equal to the existing F Both defaults belong to the same admitted quota range. Maximum quota b→b+1b→ b+1 F gains weight-(b+1)(b+1) targets New exposure bound and an all-source-witness exclusion proof; core remains sound. Replace the checker Depends on its accepted behavior Re-establish gap and task soundness; syntax admission is insufficient. Table 2: A concrete update contract. All quota languages here remain in P; these edits are not claims of learned recursive improvement. 8.3 Selection error across an adaptive improvement run SIFT uses pairwise learned-judge comparisons to prioritize a self-improvement search, with expensive task evaluations reserved for selected candidates [24]. Its ranking signal has a different role from a sound terminal verifier. AI4AI-Bench instead evaluates training-algorithm changes through fresh runs under a hidden fixed evaluator [25]. Both make the distinction between search feedback and final acceptance operationally important. Probabilistic acceptance needs a second accounting level when many candidate versions are compared. Let BiB_i be the event that the iith selection call accepts a candidate that violates a separately specified improvement criterion. Let ℋi−1H_i-1 contain the available history and selected candidate just before that call’s fresh evaluation randomness. Proposition 8.2 (Finite adaptive selection budget). Suppose a run makes at most M selection calls, including rejected candidates. If for every reachable pre-call history Pr(Bi∣ℋi−1)≤δi (B_i _i-1)≤ _i for fixed nonnegative budgets δi _i, then Pr(⋃i=1MBi)≤∑i=1Mδi. \! ( _i=1^MB_i )≤ _i=1^M _i. In particular, if each invalid fixed candidate has per-trial false acceptance probability at most 1/31/3, evaluated with independent fresh coins after the candidate is fixed, an odd majority size N≥18log(M/δ)N≥ 18 (M/δ) gives a total false-selection probability at most δ for 0<δ<10<δ<1. The conditional guarantee must cover each selection call; summing these budgets controls the risk of any false selection. The proof is in Appendix A.6. This is a standard probability bound applied to stage selection; independence between different calls is unnecessary when the conditional bound holds. Its premise concerns the improvement criterion and is not supplied merely by the tuple-level gap of a deployed checker. A pointwise error bound for invalid candidates under the selection rule must be established separately. Good average judge accuracy does not supply it. Nor do fresh decoding coins repair adaptive overfitting to a repeatedly reused benchmark; the evaluation data and feedback policy require their own validity argument [17]. The finite audit’s three-call example gives the concrete risk: three independent opportunities to accept a fixed invalid candidate with probability 1/41/4 each yield probability 37/6437/64 of at least one false acceptance. In a finite experiment, versioning the agent, improver, and evaluator separately, fixing the improvement criterion, recording all selection calls, and separating selection feedback from final evaluation make an RSI claim auditable. Establishing asymptotic frontier escape remains an additional obligation beyond demonstrating held-out performance gains. 9 Verifier scope, related work, and limitations 9.1 A realizable bounded-error contract The pointwise condition is restrictive but has concrete algorithmic instances. Consider checking AB=CAB=C for supplied n×n× n matrices over 2F_2. Draw a uniform v∈2nv _2^n and accept if A(Bv)=CvA(Bv)=Cv, repeating twice independently and requiring both tests to pass. This is the standard randomized matrix-product check [6]. Correct products pass with probability one; incorrect products pass both independent tests with probability at most 1/41/4. Thus the gap and task soundness hold uniformly. The row argument is in Appendix A.8. Each test uses quadratic field operations after the matrices are provided. This example illustrates a valid probabilistic terminal checker; it is not a separation from deterministic polynomial time. By contrast, an LLM judge may confidently favor an incorrect answer on an identifiable subset. Its probabilities can satisfy the gap while its task soundness fails. Calibration of aggregate scores cannot prove either universal condition. Abstention is useful only with a proved coverage and error contract on the retained domain, or a sound fallback whose combined acceptance is analyzed explicitly. Merely removing uncertain examples does not remove confident mistakes. Stochastic proposal generation with an exact terminal checker can still use the exact stage semantics if the admissible transcript relation is justified; that semantics leaves production probabilities unmodeled. 9.2 Related work Bounded alternation and the polynomial hierarchy supply the deterministic background [2]. Arthur–Merlin systems distinguish when verifier coins are visible to a witness [5]; our hidden-terminal-coin, pointwise-gap model is a particular restricted semantics. The classical randomized hierarchy bound supplies the sandwich proof [3, 4]. These results classify languages. The stage layer adds an explicit comparison between default support and all support admitted by one interface, together with refactoring and transition semantics. Debate uses adversarial interaction to extend what a bounded judge can evaluate [7]. Here a universal block means every bounded challenge under the declared rules, and a learned debater does not automatically realize it. Proof certificates provide another way to discharge a universal claim on restricted families. Our certificate-substitution result isolates the soundness, completeness, and size conditions needed for that comparison. Test-time scaling studies how compute allocation affects performance, including search against verifiers and iterative refinement [8]. Reflexion uses feedback and episodic memory to improve subsequent trials without weight updates [9]. These mechanisms motivate distinct search-policy and support-interface coordinates. Their empirical success does not alone establish which stage frontier changed. Likewise, studies of LLM judges document agreement with human preferences alongside systematic biases [10], and studies of intrinsic self-correction identify limits without external feedback [11]. Such measurements concern particular distributions and protocols; they do not establish the pointwise verification contracts used here. The MAST study further separates failures of system design, inter-agent coordination, and task verification [27]. This motivates recording the location of a failure rather than treating additional agents as evidence of stronger verification. 9.3 Limitations The results classify declared protocol families, not latent intelligence, training dynamics, or the probability that a model discovers a solution. Existential witnesses and worst-case universal moves idealize possible verification structure. A finite execution policy requires its own efficiency and reliability analysis. There is no claim that inference scaling must numerically plateau, that more support always helps, or that a changed stage must escape its predecessor’s frontier. The pointwise-gap model leaves average-case judges, distribution shift, and correlated errors unresolved. Randomized exposure can be represented at the level of admissible traces only when that relation is itself justified; reliable generation probabilities require an additional semantic object. Public coins require a different quantifier order. The strictness of the randomized hierarchy and its relation to standard MA beyond the stated inclusion are not settled here. The synthetic completeness constructions demonstrate expressive capacity, and the finite audits check concrete examples; neither constitutes empirical validation of frontier claims for large deployed systems. 10 Conclusion Verification provides a precise basis for distinguishing mechanisms of self-improvement in agentic AI. The native/frontier pair records what a declared interface can accept with default support and with all permitted support. Exact verification and probabilistic verification with a uniform gap share this language-based foundation under task-relative soundness. Amplification preserves the frontier; making optional support native can enlarge native reach within it; and escape requires a failure of semantic authority or exposure containment. Depth adds a separate non-compilability constraint under explicit complexity assumptions. Recursive self-improvement introduces both a changing agent and a process that proposes and selects its successors. Under a common sound interpreter, fixed protocol, and uniform resource and gap contracts, bounded self-modification remains in the same verification class, even when a successor escapes the particular predecessor’s frontier. Separately, a conditional-error budget controls false selection over adaptive candidate comparisons. These structural and statistical results permit empirical gains within a fixed frontier and leave unbounded improvement processes outside their scope. Together with the finite audits, they turn claims about stronger verification and self-improvement into explicit, testable obligations on correctness, admissible evidence, resources, and selection error. AI tool use OpenAI’s Codex assisted with manuscript revision, literature synthesis, proof development and checking, and preparation of executable artifacts and figures. The author is responsible for the paper’s content. The scope of the executable and formal checks is specified in Appendix C. References [1] Y. Duan, Y. Liu, Z. Tang, H. Chen, J. Zhou, et al. The last AI built by humans: Toward genuine recursive self-improvement. September 2026, version 3, September 22. arXiv:2609.11873v3. [2] A. K. Chandra, D. C. Kozen, and L. J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114–133, 1981. doi:10.1145/322234.322243. [3] M. Sipser. A complexity theoretic approach to randomness. In STOC, p. 330–335, 1983. doi:10.1145/800061.808762. [4] C. Lautemann. BPP and the polynomial hierarchy. Information Processing Letters, 17(4):215–217, 1983. doi:10.1016/0020-0190(83)90044-3. [5] L. Babai and S. Moran. Arthur–Merlin games: A randomized proof system, and a hierarchy of complexity classes. Journal of Computer and System Sciences, 36(2):254–276, 1988. doi:10.1016/0022-0000(88)90028-1. [6] R. Freivalds. Fast probabilistic algorithms. In Mathematical Foundations of Computer Science 1979, LNCS 74, p. 57–69. Springer, 1979. doi:10.1007/3-540-09526-8_5. [7] G. Irving, P. Christiano, and D. Amodei. AI safety via debate. 2018. arXiv:1805.00899. [8] C. Snell, J. Lee, K. Xu, and A. Kumar. Scaling LLM test-time compute optimally can be more effective than scaling model parameters. 2024. arXiv:2408.03314. [9] N. Shinn, F. Cassano, E. Berman, A. Gopinath, K. Narasimhan, and S. Yao. Reflexion: Language agents with verbal reinforcement learning. Advances in Neural Information Processing Systems, 36, 2023. arXiv:2303.11366. [10] L. Zheng, W.-L. Chiang, Y. Sheng, S. Zhuang, Z. Wu, Y. Zhuang, Z. Lin, Z. Li, D. Li, E. P. Xing, H. Zhang, J. E. Gonzalez, and I. Stoica. Judging LLM-as-a-judge with MT-Bench and Chatbot Arena. Advances in Neural Information Processing Systems, 36, 2023. arXiv:2306.05685. [11] J. Huang, X. Chen, S. Mishra, H. S. Zheng, A. W. Yu, X. Song, and D. Zhou. Large language models cannot self-correct reasoning yet. 2023, revised 2024. arXiv:2310.01798. [12] J. Zhang, S. Hu, C. Lu, R. Lange, and J. Clune. Darwin Godel Machine: Open-ended evolution of self-improving agents. 2025, revised March 2026. arXiv:2505.22954v3. [13] D. Srikanth, B. Zhao, D. Xu, Y. Wu, and Z. Jiang. Recursive self-improvement of AI research agents. September 22, 2026. arXiv:2609.26457v1. [14] S. Zhu, S. Fan, X. Wang, W. Wu, K. Zhou, and B. Huang. RSIAgent: Autonomous exploration for recursive self-improvement in new environments. September 2026. arXiv:2609.15364v2. [15] Google DeepMind. AlphaEvolve: How our Gemini-powered coding agent is scaling impact across fields. May 7, 2026. Google DeepMind research update. [16] W. Hoeffding. Probability inequalities for sums of bounded random variables. Journal of the American Statistical Association, 58(301):13–30, 1963. doi:10.1080/01621459.1963.10500830. [17] C. Dwork, V. Feldman, M. Hardt, T. Pitassi, O. Reingold, and A. Roth. Preserving statistical validity in adaptive data analysis. In STOC, p. 117–126, 2015. arXiv:1411.2664. [18] E. Zelikman, E. Lorch, L. Mackey, and A. T. Kalai. Self-Taught Optimizer (STOP): Recursively self-improving code generation. COLM, 2024. arXiv:2310.02304v3. [19] J. Zhang, B. Zhao, W. Yang, J. Foerster, J. Clune, M. Jiang, S. Devlin, and T. Shavrina. Hyperagents. March 2026. arXiv:2603.19461v1. [20] J. Lin, S. Liu, C. Pan, L. Lin, S. Dou, Z. Xi, X. Huang, H. Yan, Z. Han, T. Gui, and Y.-G. Jiang. Agentic harness engineering: Observability-driven automatic evolution of coding-agent harnesses. April 2026, revised May 2026. arXiv:2604.25850v4. [21] L. A. Agrawal, S. Tan, D. Soylu, N. Ziems, R. Khare, K. Opsahl-Ong, A. Singhvi, H. Shandilya, M. J. Ryan, M. Jiang, C. Potts, K. Sen, A. G. Dimakis, I. Stoica, D. Klein, M. Zaharia, and O. Khattab. GEPA: Reflective prompt evolution can outperform reinforcement learning. 2025, revised February 2026. arXiv:2507.19457v2. [22] J. Zhang, J. Xiang, Z. Yu, F. Teng, X. Chen, J. Chen, M. Zhuge, X. Cheng, S. Hong, J. Wang, B. Zheng, B. Liu, Y. Luo, and C. Wu. AFlow: Automating agentic workflow generation. 2024, revised April 2025. arXiv:2410.10762v4. [23] Q. Zhang, C. Hu, S. Upasani, B. Ma, F. Hong, V. Kamanuru, J. Rainton, C. Wu, M. Ji, H. Li, U. Thakker, J. Zou, and K. Olukotun. Agentic context engineering: Evolving contexts for self-improving language models. ICLR, 2026. arXiv:2510.04618v3. [24] X. Fu, A. Kulanthaivelu, and Y. Yamada. Self improvement via fast tree-search. September 17, 2026. arXiv:2609.19526v1. [25] Y. Chi, W. Li, D. Hong, X. Wang, M. Gao, K. Yang, B. He, Y. Zheng, C. Xiao, and Q. Na. AI4AI-Bench: Benchmarking LLM agents in algorithmic design for recursive self-improvement. August 2026. arXiv:2608.20318v1. [26] H. Zhang, S. Zhang, K. Li, C. Zhang, Y. Chen, Y. Zhang, L. Bai, and S. Hu. Self-Harness: Harnesses that improve themselves. June 2026, revised August 2026. arXiv:2606.09498v3. [27] M. Cemri, M. Z. Pan, S. Yang, L. A. Agrawal, B. Chopra, R. Tiwari, K. Keutzer, A. Parameswaran, D. Klein, K. Ramchandran, M. Zaharia, J. E. Gonzalez, and I. Stoica. Why do multi-agent LLM systems fail? 2025, revised October 2025. arXiv:2503.13657v3. Appendix A Proofs of the main results The notation and assumptions are those of Sections 2–3. All object domains remain fixed unless a construction explicitly declares a new encoding. Each proof below links to its statement in the main text. A.1 Stage languages and deterministic recovery Proof of Proposition 3.4. Default support is among the permitted supports, yielding the first inclusion; soundness yields the second. For frontier membership, guess σ,t,zσ,t,z in the leading existential block with y1y_1, check exposure, and use the predicate ExpS∧CoreSExp_S _S under the remaining quantifiers. Exposure is deterministic and independent of the later moves, so this predicate preserves the pointwise gap and adds no alternation. The native case fixes σ=σ0σ= _0. With no coins all acceptance probabilities are zero or one, and the same construction has a deterministic polynomial-time matrix. ∎ Proof of Theorem 3.5. Choose pointwise-gap verifiers V0,V1V_0,V_1 for the two languages, padding their move and coin lengths to common polynomial bounds and ignoring padding. Set R(x,z)⇔z=1∧x∈L1R(x,z) z=1 x∈ L_1. Default support exposes tag t=0t=0; one optional support exposes t=1t=1. On output z=1z=1 and transcript tag t=it=i, the core runs ViV_i; it rejects other encodings. Native acceptance gives L0L_0, and optional support gives L0∪L1=L1L_0∪ L_1=L_1. Soundness follows from the inclusion of languages. Deterministic ViV_i give the exact construction. ∎ A.2 False acceptance and majority amplification Proof of Proposition 4.1. Choose a proper language L∈L∈ NP with certificate predicate V(x,y)V(x,y) and set R(x,z)⇔z=1∧x∈LR(x,z) z=1 x∈ L. Expose only t=εt= . For z=1z=1, let the core accept if V(x,y)=1V(x,y)=1 or r=0n+2r=0^n+2. All other encodings are rejected. Each tuple accepts with probability either 11 or 2−(n+2)≤1/42^-(n+2)≤ 1/4, so the gap holds. Bounded-error acceptance has frontier exactly L, while an existential lucky tape accepts every input. ∎ Proof of Theorem 4.2. Let gN(p)g_N(p) be the probability that an odd majority accepts when each trial accepts with probability p. For N=2m+1N=2m+1, direct binomial expansion gives g2m+3(p)−g2m+1(p)=(2m+1m)pm+1(1−p)m+1(2p−1).g_2m+3(p)-g_2m+1(p)= 2m+1mp^m+1(1-p)^m+1(2p-1). Consequently gN(p)≥pg_N(p)≥ p for p≥1/2p≥ 1/2 and gN(p)≤pg_N(p)≤ p for p≤1/2p≤ 1/2. In particular, the high and low sides of the gap remain on their respective sides for every odd N, including N=1N=1. The standard independent Bernoulli tail bound [16] gives error at most exp(−2N(1/6)2)=e−N/18 (-2N(1/6)^2)=e^-N/18. Thus DS[N]=DSD_S^[N]=D_S pointwise. Applying the same quantifiers and exposure predicates proves every claimed semantic equality and preserves task soundness. ∎ A.3 Hierarchy bounds and derandomization Proof of Theorem 4.3. The first inclusions use zero coins. For the upper bound, the total thresholded matrix D(x,y→)D(x, y) is in BPP. If the last block is existential, substitute its classical Σ2 _2 P representation ∃u∀vB∃ u∀ v\,B; if universal, substitute its Π2 _2 P representation ∀u∃vB′∀ u∃ v\,B . Merging adjacent blocks of the same type leaves k+1k+1 blocks. The universal-start argument is identical with the initial quantifier reversed. ∎ Proof of Theorem 4.4. For (i), choose L∈Σ1∖L∈ _1 RV NP and use Theorem 3.5 with L0=L1=L_0=L_1=L. Exact depth-one frontiers belong to NP by Proposition 3.4 and cannot equal L. For (i), DSD_S is a single uniform BPP language on the encoded tuple. Under = BPP= P it has a uniform deterministic polynomial-time decider. Use that decider as the new terminal core, retaining all original domain checks. Pointwise equality of matrices preserves quantified acceptance and soundness. The same substitution proves the class equalities. ∎ A.4 Guard-transfer invariance Proof of Proposition 5.2. Guarding the core multiplies its acceptance probability by g∈0,1g∈\0,1\, so it preserves the gap and changes the threshold matrix to g∧DSg D_S. The guard is independent of the moves and can pass through their nonempty quantifier domains. Both representations therefore induce the same fused matrix HS(x,σ,z,t,y→)=ExpS(x,σ,t)∧DS(x,z,t,y→).H_S(x,σ,z,t, y)=Exp_S(x,σ,t) D_S(x,z,t, y). Quantifying it with default or existential support recovers native or frontier membership. ∎ A.5 Depth obstructions and certificate substitution Proof of Theorem 6.1. For (i) choose L∈Σk+1∖ΣkL∈ _k+1 P _k P, set RL(x,z)⇔z=1∧x∈LR_L(x,z) z=1 x∈ L, and realize native reach L by the exact case of Theorem 3.5. Every sound exact depth-k source has FRL(S)∈ΣkF_R_L(S)∈ _k P and FRL(S)⊆LF_R_L(S) L. If its frontier covered L, the two sets would be equal, contradicting the choice of L. For (i), the randomized classes are nested by appending ignored dummy blocks; a strict adjacent inequality therefore supplies a separator. Use the same argument and randomized completeness and placement. For (i), choose L∈Σk+2∖Σk+1L∈ _k+2 P _k+1 P and an exact target with native reach L. Randomized source frontiers lie in Σk+1 _k+1 P by Theorem 4.3; soundness again forces containment in L. Coverage would force the forbidden equality. ∎ Proof of Proposition 6.2. Retain the polynomial-time guard G, substitute the certificate equivalence only where G=1G=1, and merge a,πa,π into one existential block. The resulting language is in NP. A Σ2 _2 P-complete language in NP puts all of Σ2 _2 P in NP under polynomial reductions; the opposite inclusion is standard. With soundness alone only the forward implication from certified to universal acceptance is available. ∎ A.6 Bounded self-modification and adaptive selection Proof of Proposition 8.1. Include h,c,σ,t,zh,c,σ,t,z with the first existential move and use the matrix V(x,h,c,σ,t,z,y→,r)=A(x,h,c)∧E(x,h,c,σ,t)∧C(x,h,c,z,t,y→,r).V(x,h,c,σ,t,z, y;r)=A(x,h,c) E(x,h,c,σ,t) C(x,h,c,z,t, y;r). Each conjunct is interpreted by its single uniform algorithm, including the declared domain checks; the predicates A,EA,E precede and do not depend on the verification moves. Invalid records reject with probability one. Valid records inherit the candidate’s gap, so V is a total polynomial-time randomized predicate with the required gap. Move-independent deterministic guards commute with the nonempty quantifier domains. Thus quantifying V recognizes exactly LenvL_ env without adding a block. For the native union, substitute the uniformly computed default support for σ. Quantified soundness of every admitted candidate makes the enclosing language sound for R. Without coins the same construction has a deterministic matrix. ∎ Proof of Proposition 8.2. Average the conditional bounds over histories and apply the union bound. Unused calls have empty bad events. For the last claim, the independent bounded-variable tail inequality [16] bounds each call’s majority error by e−N/18≤δ/Me^-N/18≤δ/M, as in Theorem 4.2. Sum over the calls. ∎ Countable selection budgets. For a countable sequence, budgets δi=δ/2i _i=δ/2^i still give total error at most δ under the same conditional premise. This probability statement does not imply a uniform polynomial runtime for an infinite run. A.7 The quota-enforced XOR family Proof of Proposition 7.1. For each j, evaluating on the basis vector eje_j shows that a correct canonical program includes index j if and only if aj=1a_j=1. Thus there is exactly one correct canonical program, of reference count ‖a‖0\|a\|_0. Conversely that program agrees on all inputs by linearity over 2F_2. The core is therefore sound and complete for this restricted task. It is the same polynomial-time algorithm at every dimension and quota; all encodings, quota comparisons, and default supports are uniformly polynomial-time checkable or computable. Using O(dlogd)O(d d) encoded objects and an ignored move supplies an exact depth-one stage. The unique correct program is native precisely when its length is at most b0(d)b_0(d), and some allowed support admits it precisely when its length is at most B(d)B(d). This proves the two language formulas. For a target of weight b+1b+1, every source-exposed transcript has at most b references, so none can be the correct program. The expanded stage exposes that program natively. The exclusion argument covers all source supports and transcripts; failure to observe a successful source run is not used. The uniform and biased policies assign positive probability to every program. When the correct program is admissible, its masses are 2−d2^-d and 1/2+2−(d+1)1/2+2^-(d+1), whose ratio is 2d−1+1/22^d-1+1/2. Taking d arbitrarily large proves the unbounded ratio without changing either language. Below the correct program’s quota both success probabilities are zero. Independence of M attempts gives 1−(1−p)M1-(1-p)^M. These are probabilities of producing an admissible correct output with the exact core, not of obtaining one lucky acceptance from a noisy judge. Finally, summing (dj) dj over the admitted weights gives the reported finite counts. ∎ An improver can modify either proposal policy while the harness keeps the quota and checker fixed. Such updates preserve this envelope regardless of whether the improver itself is editable. Admission of an arbitrary replacement checker requires a separate soundness argument, as in Proposition 8.1. The example isolates these obligations without claiming to explain how a learned improver discovers a useful policy. A.8 The randomized matrix-product check For the checker in Section 9, correct products pass every test. If AB≠CAB≠ C, choose a nonzero row d of AB−CAB-C. The dot product dvdv is a uniform bit for uniform v∈2nv _2^n, so Pr(dv=0)=1/2 (dv=0)=1/2. Acceptance implies dv=0dv=0, giving a one-test false-acceptance probability at most 1/21/2. Independent repetitions therefore both accept with probability at most 1/41/4. The same bound holds for every incorrect matrix triple, establishing the pointwise gap and task soundness claimed in the main text. Appendix B Representation machinery and supporting constructions B.1 Simulation and support normalization Definition B.1 (Simulation). Write S⪯simTS simT when the depths agree and a polynomial-time map ϕ(x,t)φ(x,t) maps NatS(x)Nat_S(x) into NatT(x)Nat_T(x) and ExpS∗(x)Exp_S^*(x) into ExpT∗(x)Exp_T^*(x), and preserves accepted-input membership on each mapped transcript from S to T. Proposition B.2 (Simulation and support normalization). Mutual simulation preserves native reach and frontier. Every stage has a representation with the same native reach and frontier and just two support states, carrying optional support payloads inside tagged transcripts. Proof. For simulation, map a witnessing transcript through ϕφ and apply the preserved acceptance condition; mutual simulation gives both inclusions. For normalization, default support exposes ⟨0,t⟩ 0,t precisely when t was native, and optional support exposes ⟨1,σ,t⟩ 1,σ,t precisely when ExpS(x,σ,t)Exp_S(x,σ,t). The new core decodes the record and runs the old core, rejecting invalid records. A polynomial enlargement accommodates the encoding while retaining the original decoded bounds. Decoding is surjective onto the old exposed transcripts, generally not injective because several support states can expose the same t. Existential acceptance needs only this surjectivity, giving equality of both languages. ∎ B.2 The local invariant of guard transfer Proposition B.3 (Local guard invariant). At a fixed tuple, every observation h(e,d)h(e,d) of exposure and thresholded acceptance that is invariant under Boolean guard transfer factors uniquely through e∧de d. Proof. Invariance means h(e∧g,d)=h(e,g∧d)h(e g,d)=h(e,g d). Set e=1e=1 and g=e′g=e to obtain h(e′,d)=h(1,e′∧d)h(e ,d)=h(1,e d). Thus h(e,d)=f(e∧d)h(e,d)=f(e d) for f(b)=h(1,b)f(b)=h(1,b); both Boolean values are attained, giving uniqueness. ∎ The factorization is local and concerns this specified family of refactorings; it is not a completeness theorem for every possible representation change. B.3 Separate same-depth escape constructions Proposition B.4 (Two independent same-depth realizations). For any L0⊊L1L_0 L_1 in Σk _k RV, frontier escape can be realized at depth k by changing only the core, or by changing only exposure. Proof. Use R(x,z)⇔z=1∧x∈L1R(x,z) z=1 x∈ L_1 and verifiers V0,V1V_0,V_1. All constructed cores reject outputs other than z=1z=1. For a core-only change, both stages expose only t=εt= and use V0,V1V_0,V_1 respectively. For an exposure-only change, fix one core that uses ViV_i on tag i on all transcripts, including unexposed ones. The source exposes only tag 00 under every support state; the target exposes both tags already under default support. Thus the source frontier is L0L_0, target native reach is L1L_1, and the core is unchanged even on the newly exposed tag. ∎ The deterministic version follows with exact verifiers. B.4 Finite chains of same-depth frontier expansion Proposition B.5. Given a finite chain L0⊊⋯⊊LmL_0 ·s L_m in Σk _k RV and any sequence of labels bi∈core,supportb_i∈\core,support\, there are sound depth-k stages with native and frontier languages both equal to LiL_i such that transition i changes only the component indicated by bib_i. Proof. Set R(x,z)⇔z=1∧x∈LmR(x,z) z=1 x∈ L_m and choose a pointwise-gap verifier ViV_i for each LiL_i, with common padded bounds. Initially expose one active tag using V0V_0. Every core rejects z≠1z≠ 1. For every future support transition i, prepare a distinct dormant tag whose core already uses Vi+1V_i+1. The core is defined on all tags, independently of exposure. Both native and conservative exposure contain exactly the active tags. At a support transition, expose its prepared tag and leave the whole core unchanged. At a core transition, keep exposure fixed and replace the verifier on every active tag by Vi+1V_i+1; leave all dormant tags unchanged. At step i+1i+1, old active languages lie in Li+1L_i+1 and either one new active tag or every active tag realizes Li+1L_i+1. Thus the union is exactly Li+1L_i+1. Soundness holds because even dormant languages lie within LmL_m. The strict chain gives frontier escape at every step. Exact verifiers give the exact version. Finiteness of the chain permits all tags and bounds to be hardwired; no uniform infinite-chain claim follows. ∎ Appendix C Finite verification and reproduction Code availability. The accompanying arXiv source package places the manuscript at its root and the executable artifacts, tests, saved results, and Lean kernel in anc/. The ancillary artifact version is 2026-10-07-arxiv. Its MANIFEST.json records SHA-256 hashes for every ancillary payload file. Python artifacts use only the standard library and were checked with Python 3.10.9; the Lean kernel specifies Lean 4.29.1. From anc/, python3 reproduce.py runs the regressions and compares regenerated results with the saved records. PDF compilation separately requires a LaTeX distribution with the packages declared in the root main.tex. The vector figures are supplied as TikZ/PGFPlots source in figures/ at the package root. Their three numeric tables are generated by anc/integrated/figures/generate_data.py using exact binomial and rational arithmetic. The generator checks the policy conditions against the XOR audit and records source and data hashes; plotted curves are analytic, not sampled measurements. The ancillary files include complementary verification artifacts. The exact artifact enumerates the bounded patching task and checks certificate binding, hidden counterexamples, native/frontier input sets, and accepted-output projections. It also includes Boolean QBF and compact XOR-circuit examples. A Lean file checks a propositional kernel for guard transfer, accepted-game invariance, and certificate substitution; it does not formalize the probabilistic hierarchy or prove an asymptotic separation. From anc/, the exact regressions run as follows:python3 -m unittest discover -s code/exact_audit -p ’test_*.py’ -v The self-contained additional artifact is integrated/audit.py:python3 integrated/audit.py It computes the four-tape noisy-checker probabilities and three-call majority probabilities exactly, checks the exposure/internalization chain, evaluates the quantified-soundness counterexample, exhaustively verifies Boolean guard factorization, and tests the two-trial matrix check on all 2×22× 2 Boolean matrix triples. Its output is a JSON record with the source hash, declared domains, and exact fractions. The finite matrix test supplements the general row argument in Appendix A.8; it does not replace that proof. From the same anc/ directory, the growing XOR harness and audit run as follows:python3 -m unittest discover -s integrated -p ’test_xor_envelope.py’ -v python3 integrated/xor_envelope.py Its tests independently compare the symbolic checker to exhaustive truth tables for d≤4d≤ 4, check malformed and mismatched records, and verify actual transcript inclusion for internalization. Its JSON report records exact language counts and proposal probabilities for d≤6d≤ 6, with the policy target, selected stage, default and optional quotas, and attempt count explicitly recorded. The escape witness is a separate target. At d=6d=6, the policy target has weight three and uses optional quota three; under default quota zero its success probability is zero for both policies. The separate patch report uses exposure_atom_inclusion for fact sets and native_to_frontier_traninclusion for the exposure premise of Theorem 5.3; these diagnostics need not agree. Claim boundaries. All finite examples use explicitly declared small domains. The polynomial hierarchy statements concern unbounded input families and follow from their proofs and stated assumptions. No finite audit result is reported as evidence for a complexity-class separation, learned-verifier calibration, or a frontier measurement of an undeclared deployment. Appendix D Self-improvement mechanisms and comparative evidence The mechanisms in Table 3 suggest distinct stage comparisons. The middle column summarizes reported designs; the right column gives our proposed connection to the stage model. These connections are audit questions, not established classifications of the cited implementations. Table 3: Mechanism-level comparison of self-improvement research. Research line Reported mechanism Stage comparison and evidence needed Autonomy and inherited improvement Duan et al. organize RSI by control over execution, strategy, experience, deployment adaptation, and inherited improvement mechanisms. They separate structural from effective recursion [1]. An autonomy level does not determine k. Record accepted-language changes separately from proposal efficiency and successor quality. A fixed enclosing class can accommodate both inherited meta-updates and empirical gains. Prompt and context adaptation GEPA reflects on execution traces to evolve prompts; ACE incrementally maintains playbooks; RSIAgent carries frozen memory into evaluation [21, 23, 14]. Declare which context was already available through optional support. Compare memory admissibility and use under matched task and output contracts. Workflow search AFlow uses Monte Carlo tree search over code-represented workflows and execution feedback [22]. Separate a better policy over existing traces from a changed trace grammar. Adding a critic node does not establish universal challenge semantics. Agent and harness code DGM retains an archive of self-modified agents. AHE exposes editable components and records predicted effects; Self-Harness validates proposed edits with regression tests [12, 20, 26]. Version the permitted programs, tool behavior, and terminal checker. An edit may affect exposure, acceptance, or only search efficiency; its file location does not determine its semantic role. Editable improvers STOP optimizes the improver’s own program. Hyperagents jointly exposes task and meta-agent code to modification. AIDE2 explores research-agent improvement across successive versions [18, 19, 13]. Version SiS_i, UiU_i, and JiJ_i separately. Measure the updated improver on common starting agents and budgets, and identify any fixed outer search or evaluation process. Search evaluation SIFT aggregates pairwise judge preferences through a Bradley–Terry model to guide parent selection and evaluation priority [24]. Treat ranking feedback as a search signal unless its separate acceptance contract is established. Include all selection calls in the error and cost accounting. Training-algorithm design AI4AI-Bench uses ten research repositories and reruns candidate training algorithms from scratch under a hidden fixed evaluator [25]. Keep algorithm changes distinct from runtime tuning. The benchmark’s normalized utility measures performance under its protocol; it is neither a soundness probability nor a frontier measurement. Program discovery AlphaEvolve uses executable evaluation to guide program search and reports applications across scientific domains [15]. Declare the candidate language and correctness objective. Distinguish a better discovered program from a change to the agent that discovers programs. D.1 Comparing task improvement and improver improvement The RSI survey’s Headroom-Closed Index summarizes benchmark scores; its post-2026 extension is explicitly illustrative [1]. Neither is the closure frontier defined here. Its case studies supply motivation and mechanisms to examine, not evidence that their implementations satisfy our uniform verification contracts. Conversely, our closure results do not decide whether those mechanisms produce better successors. Hyperagents evaluates the capacity of a meta agent to generate better task agents with an improvement@k metric. In that comparison the meta agent is held fixed, and the best child is selected using validation performance before test performance is measured [19]. This provides a concrete precedent for separating deployed-task scores from the ability to produce better successors. Its main experiments retain a fixed task distribution and outer selection/evaluation processes, which delimit the reported recursion. A comparison under the present model first fixes the task relation, candidate grammar, evaluator, initial deployed stage, and resource accounting. It then compares the old and new improvers with the same starting information and reports held-out improvement as a function of evaluation calls, tokens, and elapsed compute. A fixed number of generations alone need not equalize cost when candidates have different runtimes. An ablation that freezes the improver but continues task-agent search separates improvements to the search procedure from additional search effort. These measurements concern discovery and selection; semantic frontier escape additionally needs the evidence in Section 7.4. D.2 Separating diagnosis, ranking, and acceptance AHE reports that its predicted fixes are more informative than its predicted regressions, with many regressions remaining unforeseen [20]. SIFT explicitly treats its judge as an intermediate ranking signal rather than a certificate of downstream superiority [24]. Both support keeping diagnostic feedback separate from the evidence used to accept a successor. Self-Harness makes regression testing part of that selection loop [26]. Under our definitions, changing the selection test or evaluator must be recorded separately from changing the candidate agent. A reused evaluation set can become part of the effective search feedback even when the evaluator’s source code stays fixed. Fresh execution from scratch and hidden final evaluation, as used by AI4AI-Bench [25], help specify an experimental comparison; they do not by themselves establish a uniform mathematical soundness contract. This is why Proposition 8.2 states a conditional-error premise instead of inferring one from benchmark scores.