Verification and Self-Improvement in Agentic AI: Foundations and Limits

# Verification and Self-Improvement in Agentic AI:Foundations and Limits
Source: [https://arxiv.org/html/2610.10611](https://arxiv.org/html/2610.10611)
###### 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𝖯\\Sigma\_\{k\}^\{\\mathsf\{P\}\}\\subseteq\\Sigma\_\{k\}^\{\\mathsf\{RV\}\}\\subseteq\\Sigma\_\{k\+1\}^\{\\mathsf\{P\}\}; strict enlargement and depth separation require explicit complexity assumptions, while𝖡𝖯𝖯=𝖯\\mathsf\{BPP\}=\\mathsf\{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\.

## 1Introduction

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](https://arxiv.org/html/2610.10611#S7)distinguishes all three changes\.

Figure[1](https://arxiv.org/html/2610.10611#S1.F1)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′=LL^\{\\prime\}=LF′=FF^\{\\prime\}=FHigher success probability;same accepted\-input sets\.LLL′L^\{\\prime\}F′=FF^\{\\prime\}=FL⊊L′⊆FL\\subsetneq L^\{\\prime\}\\subseteq F;more default access\.FFF′F^\{\\prime\}L′L^\{\\prime\}x⋆x\_\{\\star\}x⋆∈L′∖Fx\_\{\\star\}\\in L^\{\\prime\}\\setminus F;beyond the old frontier\.native reachclosure frontierprevious boundaryFigure 1:Three comparisons under a common task relation\. Each shape represents*task inputs*; area is schematic and does not measure probability or cardinality\. WriteL=LR​\(S\)L=\\mathrm\{L\}\_\{R\}\(S\),F=FR​\(S\)F=\\mathrm\{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 most1/31/3or at least2/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](https://arxiv.org/html/2610.10611#S9)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](https://arxiv.org/html/2610.10611#bib.bib12),[13](https://arxiv.org/html/2610.10611#bib.bib13),[14](https://arxiv.org/html/2610.10611#bib.bib14)\]\. 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](https://arxiv.org/html/2610.10611#bib.bib1)\]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](https://arxiv.org/html/2610.10611#S2)supplies the deterministic background; Section[3](https://arxiv.org/html/2610.10611#S3)defines probabilistic stages and their exact specialization\. Sections[4](https://arxiv.org/html/2610.10611#S4)–[6](https://arxiv.org/html/2610.10611#S6)establish stability, transition diagnosis, and conditional limits\. Section[7](https://arxiv.org/html/2610.10611#S7)gives executable finite examples and a declaration protocol\. Section[8](https://arxiv.org/html/2610.10611#S8)applies the framework to recursive self\-improvement\. Related work and scope limitations close the main discussion\. Appendix[A](https://arxiv.org/html/2610.10611#A1)contains the detailed proofs, Appendix[B](https://arxiv.org/html/2610.10611#A2)develops the supporting representation machinery, and Appendix[C](https://arxiv.org/html/2610.10611#A3)gives reproduction instructions\. Appendix[D](https://arxiv.org/html/2610.10611#A4)compares the self\-improvement mechanisms and their evaluation requirements\.

## 2Preliminaries: the deterministic foundation

Inputs, outputs, and messages are finite binary strings under fixed encodings\. Writen=\|x\|n=\|x\|\. A task relationR⊆X×ZR\\subseteq X\\times Zis*polynomially balanced*if there is a polynomialqqsuch thatR⁡\(x,z\)⇒\|z\|≤q⁡\(\|x\|\)R\(x,z\)\\Rightarrow\|z\|\\leq q\(\|x\|\)\. This bounds every valid encoded output\. It does not assert thatRRis decidable in polynomial time, or that a valid output can be efficiently found\. For a bounded patching task,xxcontains the program and specification, andzzis a patch of the declared maximum length\.

#### Certificates and alternating verification \(classical background\)\.

𝖯\\mathsf\{P\}is deterministic polynomial time\. A language is in𝖭𝖯\\mathsf\{NP\}if membership has a polynomial\-length certificate checked in polynomial time\. More generally, for fixedk≥1k\\geq 1, write

𝒬ky→=∃y1∀y2∃y3⋯Qkyk,\\mathcal\{Q\}\_\{k\}\\vec\{y\}=\\exists y\_\{1\}\\,\\forall y\_\{2\}\\,\\exists y\_\{3\}\\cdots Q\_\{k\}y\_\{k\},with each string ranging over a nonempty polynomially bounded domain\. A languageLLis inΣk𝖯\\Sigma\_\{k\}^\{\\mathsf\{P\}\}whenx∈Lx\\in Lis equivalent to𝒬k​y→​V​\(x,y→\)=1\\mathcal\{Q\}\_\{k\}\\vec\{y\}\\,V\(x,\\vec\{y\}\)=1for a deterministic polynomial\-time predicateVV\. The universal\-start version definesΠk𝖯\\Pi\_\{k\}^\{\\mathsf\{P\}\}, and𝖯𝖧=⋃k≥0Σk𝖯\\mathsf\{PH\}=\\bigcup\_\{k\\geq 0\}\\Sigma\_\{k\}^\{\\mathsf\{P\}\}withΣ0𝖯=𝖯\\Sigma\_\{0\}^\{\\mathsf\{P\}\}=\\mathsf\{P\}\. These are standard bounded\-alternation characterizations\[[2](https://arxiv.org/html/2610.10611#bib.bib2)\]\. There arekkquantifier blocks andk−1k\-1switches between quantifier types; “depth” below counts blocks\.

For example,∃a​∀u​∃v​V​\(x,a,u,v\)\\exists a\\,\\forall u\\,\\exists v\\,V\(x,a,u,v\)says that some proposalaahas a valid replyvvfor every challengeuu\. The reply may depend onuu, whileaacannot\. A sampled critic does not implement∀u\\forall 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*ofuupermits 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\.

𝖡𝖯𝖯\\mathsf\{BPP\}consists of languages decidable in polynomial time with two\-sided error at most1/31/3on every input\. We use it for a*tuple\-level*predicate, after the verification moves have been specified\. The classical containment

𝖡𝖯𝖯⊆Σ2𝖯∩Π2𝖯\\mathsf\{BPP\}\\subseteq\\Sigma\_\{2\}^\{\\mathsf\{P\}\}\\cap\\Pi\_\{2\}^\{\\mathsf\{P\}\}is the Sipser–Gács–Lautemann bound\[[3](https://arxiv.org/html/2610.10611#bib.bib3),[4](https://arxiv.org/html/2610.10611#bib.bib4)\]\. These background facts will locate the stage languages\. They do not identify the stage declaration of an observed product\.

## 3Probabilistic stages and exact specialization

###### Definition 3\.1\(Bounded probabilistic stage\)\.

A stage for a polynomially balanced taskRRisS=\(k,pS,σ0,ExpS,CoreS\)S=\(k,p\_\{S\},\\sigma\_\{0\},\\mathrm\{Exp\}\_\{S\},\\mathrm\{Core\}\_\{S\}\), with the following data and contracts\.

1. \(i\)k≥1k\\geq 1is fixed\. The polynomialpS​\(n\)p\_\{S\}\(n\)bounds the lengths of supportσ\\sigma, transcripttt, outputzz, and each verification moveyiy\_\{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\)\\sigma\_\{0\}\(x\)is uniformly polynomial\-time computable and admissible; we suppress its input argument when unambiguous\. All quantified domains include the empty string\.
2. \(ii\)ExpS​\(x,σ,t\)\\mathrm\{Exp\}\_\{S\}\(x,\\sigma,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\.
3. \(iii\)CoreS​\(x,z,t,y→,r\)\\mathrm\{Core\}\_\{S\}\(x,z,t,\\vec\{y\};r\)is a uniform polynomial\-time Boolean predicate\. Hererris uniform on\{0,1\}ρS​\(n\)\\\{0,1\\\}^\{\\rho\_\{S\}\(n\)\}for a declared polynomialρS\\rho\_\{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\.
4. \(iv\)On every well\-formed bounded tuplew=\(x,z,t,y→\)w=\(x,z,t,\\vec\{y\}\), the acceptance probability obeys aS\(w\):=Prr\[CoreS\(w;r\)=1\]∈\[0,1/3\]∪\[2/3,1\]\.a\_\{S\}\(w\):=\\Pr\_\{r\}\[\\mathrm\{Core\}\_\{S\}\(w;r\)=1\]\\in\[0,1/3\]\\cup\[2/3,1\]\.\(1\)DefineDS\(w\)=𝟏\{aS\(w\)≥2/3\}D\_\{S\}\(w\)=\\mathbf\{1\}\\\{a\_\{S\}\(w\)\\geq 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\.\\mathcal\{A\}\_\{S\}\(x,z,t\)\\quad\\Longleftrightarrow\\quad\\mathcal\{Q\}\_\{k\}\\vec\{y\}\\ D\_\{S\}\(x,z,t,\\vec\{y\}\)=1\.\(2\)
5. \(v\)Task\-relative soundness holds: for every exposed transcript, ExpS​\(x,σ,t\)∧𝒜S​\(x,z,t\)⟹R⁡\(x,z\)\.\\mathrm\{Exp\}\_\{S\}\(x,\\sigma,t\)\\ \\wedge\\ \\mathcal\{A\}\_\{S\}\(x,z,t\)\\quad\\Longrightarrow\\quad 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 makesDSD\_\{S\}a total𝖡𝖯𝖯\\mathsf\{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𝖡𝖯𝖯\\mathsf\{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=0\}D\(a,u\)=\\mathbf\{1\}\\\{u=0\\\}satisfies the gap, but∃a​∀u​D​\(a,u\)\\exists a\\,\\forall 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,σ\\sigmacan encode a counterexample,ttthe bounded proposal/test/repair record, and the finalzzthe patch to certify\. Any verification moves afterzzsupport 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](https://arxiv.org/html/2610.10611#S3.E2)\)\.

Input and supportx,σx,\\sigmaAdmissible recordExpS​\(x,σ,t\)\\mathrm\{Exp\}\_\{S\}\(x,\\sigma,t\)Output and movesz,𝒬k​y→z,\\mathcal\{Q\}\_\{k\}\\vec\{y\}Terminal checkerCoreS​\(w,r\)\\mathrm\{Core\}\_\{S\}\(w;r\)Hidden coinsrrFigure 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\)\}\.\\mathrm\{Nat\}\_\{S\}\(x\)=\\\{t:\\mathrm\{Exp\}\_\{S\}\(x,\\sigma\_\{0\},t\)\\\},\\qquad\\mathrm\{Exp\}\_\{S\}^\{\*\}\(x\)=\\\{t:\\exists\\sigma\\ \\mathrm\{Exp\}\_\{S\}\(x,\\sigma,t\)\\\}\.All objects are bounded as in Definition[3\.1](https://arxiv.org/html/2610.10611#S3.Thmtheorem1)\. Define

LR​\(S\)\\displaystyle\\mathrm\{L\}\_\{R\}\(S\)=\{x:∃t∈NatS​\(x\)​∃z​𝒜S​\(x,z,t\)\},\\displaystyle=\\\{x:\\exists t\\in\\mathrm\{Nat\}\_\{S\}\(x\)\\ \\exists z\\ \\mathcal\{A\}\_\{S\}\(x,z,t\)\\\},\(4\)FR​\(S\)\\displaystyle\\mathrm\{F\}\_\{R\}\(S\)=\{x:∃t∈ExpS∗​\(x\)​∃z​𝒜S​\(x,z,t\)\}\.\\displaystyle=\\\{x:\\exists t\\in\\mathrm\{Exp\}\_\{S\}^\{\*\}\(x\)\\ \\exists z\\ \\mathcal\{A\}\_\{S\}\(x,z,t\)\\\}\.\(5\)These symbols use bounded\-error acceptance throughout; the superscriptex\\mathrm\{ex\}will denote an exact specialization when comparison is needed\.

For a concrete instance, letx=\(1d,a\)x=\(1^\{d\},a\)specify a Boolean linear function, and lett=zt=zlist its referenced variables\. Optional support selects a quotaq≤B⁡\(d\)q\\leq B\(d\), defaulting tob0​\(d\)b\_\{0\}\(d\)\. Exposure requires\|t\|≤q\|t\|\\leq q; an exact coefficient check establishes correctness\. Native reach then requires‖a‖0≤b0​\(d\)\\\|a\\\|\_\{0\}\\leq b\_\{0\}\(d\), and the frontier requires‖a‖0≤B⁡\(d\)\\\|a\\\|\_\{0\}\\leq B\(d\)\. Section[7\.3](https://arxiv.org/html/2610.10611#S7.SS3)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\)\.

Fork≥1k\\geq 1, a languageLLbelongs toΣk𝖱𝖵\\Sigma\_\{k\}^\{\\mathsf\{RV\}\}if some polynomial\-time randomized predicateV⁡\(x,y→,r\)V\(x,\\vec\{y\};r\)has a pointwise gap on all bounded tuples and

x∈L⟺𝒬ky→\[Prr\(V\(x,y→;r\)=1\)≥2/3\]\.x\\in L\\quad\\Longleftrightarrow\\quad\\mathcal\{Q\}\_\{k\}\\vec\{y\}\\ \[\\Pr\_\{r\}\(V\(x,\\vec\{y\};r\)=1\)\\geq 2/3\]\.Πk𝖱𝖵\\Pi\_\{k\}^\{\\mathsf\{RV\}\}is the universal\-start dual\. On no\-instances the gap gives the dual quantifier formula with threshold at most1/31/3by negation\.

This is a paper\-specific notation for bounded alternation over a total𝖡𝖯𝖯\\mathsf\{BPP\}predicate\. At depth one,𝖭𝖯⊆Σ1𝖱𝖵⊆𝖬𝖠\\mathsf\{NP\}\\subseteq\\Sigma\_\{1\}^\{\\mathsf\{RV\}\}\\subseteq\\mathsf\{MA\}: the witness is chosen before the coins\. The additional pointwise restriction applies even to losing witnesses on yes\-instances, so equality with standard𝖬𝖠\\mathsf\{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](https://arxiv.org/html/2610.10611#bib.bib5)\]\.

###### Proposition 3\.4\(Placement and deterministic recovery\)\.

For a sound stage of depthkk,

LR​\(S\)⊆FR​\(S\)⊆dom⁡\(R\),LR​\(S\),FR​\(S\)∈Σk𝖱𝖵\.\\mathrm\{L\}\_\{R\}\(S\)\\subseteq\\mathrm\{F\}\_\{R\}\(S\)\\subseteq\\mathrm\{dom\}\(R\),\\qquad\\mathrm\{L\}\_\{R\}\(S\),\\mathrm\{F\}\_\{R\}\(S\)\\in\\Sigma\_\{k\}^\{\\mathsf\{RV\}\}\.An exact stage hasρS=0\\rho\_\{S\}=0, henceDS=CoreSD\_\{S\}=\\mathrm\{Core\}\_\{S\}\. Its native and frontier languages belong toΣk𝖯\\Sigma\_\{k\}^\{\\mathsf\{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](https://arxiv.org/html/2610.10611#A1.SS1)\.

###### Theorem 3\.5\(Expressive completeness of native/frontier pairs\)\.

Fixk≥1k\\geq 1andL0⊆L1L\_\{0\}\\subseteq L\_\{1\}with both languages inΣk𝖱𝖵\\Sigma\_\{k\}^\{\\mathsf\{RV\}\}\. There is a sound depth\-kkstage withLR​\(S\)=L0\\mathrm\{L\}\_\{R\}\(S\)=L\_\{0\}andFR​\(S\)=L1\\mathrm\{F\}\_\{R\}\(S\)=L\_\{1\}for a polynomially balanced taskRR\. If both languages are inΣk𝖯\\Sigma\_\{k\}^\{\\mathsf\{P\}\}, the stage can be exact\.

The proof is in Appendix[A\.1](https://arxiv.org/html/2610.10611#A1.SS1)\.

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](https://arxiv.org/html/2610.10611#S3.Thmtheorem4), it supplies the deterministic foundation without reliance on a separate paper\.

## 4What randomization changes

### 4\.1False 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∃r​CoreS=1\\exists r\\,\\mathrm\{Core\}\_\{S\}=1strictly 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](https://arxiv.org/html/2610.10611#A1.SS2)\. 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 stageSSand a polynomial\-time computable, odd positive, polynomially bounded repetition countN⁡\(n\)N\(n\)\. Replace its terminal core by a strict majority ofN⁡\(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 stageS\[N\]S^\{\[N\]\}has the sameDSD\_\{S\}, quantified acceptance, native reach, and frontier\. Its pointwise error is at moste−N/18e^\{\-N/18\}\.

Independent majority improves reliability without moving any tuple across the acceptance gap\. The proof is in Appendix[A\.2](https://arxiv.org/html/2610.10611#A1.SS2)\.

For any constant0<δ<1/20<\\delta<1/2, sufficiently many odd repetitions yield error at mostδ\\deltawith the same acceptance language, using threshold1−δ1\-\\deltafor 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](https://arxiv.org/html/2610.10611#S4.F3)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 acceptanceppMajority acceptance\(a\) Majority responseN=1N=1N=3N=3N=15N=15115599131317172121000\.250\.250\.50\.50\.750\.751137/6437/645/325/32Independent callsNN\(odd\)False\-acceptance probability\(b\) False acceptance atp=1/4p=1/4Any passMajorityFigure 3:Reliability depends on the aggregation rule\. \(a\) The exact binomial majority mapgN​\(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](https://arxiv.org/html/2610.10611#S4.Thmtheorem2)\)\. \(b\) For the same fixed false tuple with single\-call probability1/41/4, independent majority reduces false acceptance, whereas “any pass” gives1−\(3/4\)N1\-\(3/4\)^\{N\}\. At three calls these are5/325/32and37/6437/64\. Curves are analytic, with the tuple and exposure held fixed\.
### 4\.2Classical placement and conditional comparisons

###### Theorem 4\.3\(Sandwich bound\)\.

For everyk≥1k\\geq 1,

Σk𝖯⊆Σk𝖱𝖵⊆Σk\+1𝖯,Πk𝖯⊆Πk𝖱𝖵⊆Πk\+1𝖯\.\\Sigma\_\{k\}^\{\\mathsf\{P\}\}\\subseteq\\Sigma\_\{k\}^\{\\mathsf\{RV\}\}\\subseteq\\Sigma\_\{k\+1\}^\{\\mathsf\{P\}\},\\qquad\\Pi\_\{k\}^\{\\mathsf\{P\}\}\\subseteq\\Pi\_\{k\}^\{\\mathsf\{RV\}\}\\subseteq\\Pi\_\{k\+1\}^\{\\mathsf\{P\}\}\.

Replacing the terminal randomized predicate by its classical alternating representation costs at most one extra block\. The proof is in Appendix[A\.3](https://arxiv.org/html/2610.10611#A1.SS3)\.

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\)\.

1. \(i\)IfΣ1𝖱𝖵⊈𝖭𝖯\\Sigma\_\{1\}^\{\\mathsf\{RV\}\}\\not\\subseteq\\mathsf\{NP\}, some sound randomized depth\-one stage has a frontier that no exact depth\-one stage can equal\.
2. \(ii\)If𝖡𝖯𝖯=𝖯\\mathsf\{BPP\}=\\mathsf\{P\}, thenΣk𝖱𝖵=Σk𝖯\\Sigma\_\{k\}^\{\\mathsf\{RV\}\}=\\Sigma\_\{k\}^\{\\mathsf\{P\}\}andΠk𝖱𝖵=Πk𝖯\\Pi\_\{k\}^\{\\mathsf\{RV\}\}=\\Pi\_\{k\}^\{\\mathsf\{P\}\}for allkk\. 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](https://arxiv.org/html/2610.10611#A1.SS3)\.

The enlargement premise is specific to the pointwise\-gap class;𝖬𝖠≠𝖭𝖯\\mathsf\{MA\}\\neq\\mathsf\{NP\}alone does not supply it\. Failure of𝖡𝖯𝖯=𝖯\\mathsf\{BPP\}=\\mathsf\{P\}would not by itself prove strict stage\-frontier enlargement either\. These are conditional comparisons, not demonstrated advantages of a deployed neural judge\.

## 5Representation invariants and structural diagnosis

Define the transcript\-indexed accepted\-input setKS​\(x,t\)⇔∃z​𝒜S​\(x,z,t\)K\_\{S\}\(x,t\)\\iff\\exists z\\,\\mathcal\{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\)\.

WriteT⪯authST\\preceq^\{\\rm auth\}SifKT​\(x,t\)⇒KS​\(x,t\)K\_\{T\}\(x,t\)\\Rightarrow K\_\{S\}\(x,t\)for allx,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](https://arxiv.org/html/2610.10611#A2.SS1)\.

###### Proposition 5\.2\(Guard transfer\)\.

For a deterministic polynomial\-time guardg⁡\(x,t\)g\(x,t\), the stages

\(ExpS∧g,CoreS\)and\(ExpS,g∧CoreS\)\(\\mathrm\{Exp\}\_\{S\}\\wedge g,\\mathrm\{Core\}\_\{S\}\)\\quad\\hbox\{and\}\\quad\(\\mathrm\{Exp\}\_\{S\},g\\wedge\\mathrm\{Core\}\_\{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](https://arxiv.org/html/2610.10611#A1.SS4)proves the result; Appendix[B\.2](https://arxiv.org/html/2610.10611#A2.SS2)characterizes the associated local invariant\.

This invariance explains an audit limitation\. With one input and two transcriptsa,ba,b, let a source expose and accept onlyaa\. A target that exposes onlyaaand whose core accepts both transcripts has a raw authority change\. Moving the guard foraainto the target core produces an equivalent target that exposes both transcripts but accepts onlyaa; 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\)\.

IfT⪯authST\\preceq^\{\\rm auth\}SandNatT​\(x\)⊆ExpS∗​\(x\)\\mathrm\{Nat\}\_\{T\}\(x\)\\subseteq\\mathrm\{Exp\}\_\{S\}^\{\*\}\(x\)for everyxx, thenLR​\(T\)⊆FR​\(S\)\\mathrm\{L\}\_\{R\}\(T\)\\subseteq\\mathrm\{F\}\_\{R\}\(S\), regardless of their depths\. More precisely, ifx∈LR​\(T\)∖FR​\(S\)x\\in\\mathrm\{L\}\_\{R\}\(T\)\\setminus\\mathrm\{F\}\_\{R\}\(S\), every accepted target\-native transcriptttfor that input satisfies

t∉ExpS∗​\(x\)or¬KS​\(x,t\)\.t\\notin\\mathrm\{Exp\}\_\{S\}^\{\*\}\(x\)\\quad\\hbox\{or\}\\quad\\neg K\_\{S\}\(x,t\)\.

###### Proof\.

An accepted target\-nativettthat also lies inExpS∗​\(x\)\\mathrm\{Exp\}\_\{S\}^\{\*\}\(x\)and satisfiesKS​\(x,t\)K\_\{S\}\(x,t\)would witnessx∈FR​\(S\)x\\in\\mathrm\{F\}\_\{R\}\(S\), a contradiction\. Under both containment premises such a witness exists for everyx∈LR​\(T\)x\\in\\mathrm\{L\}\_\{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](https://arxiv.org/html/2610.10611#S6)\.

Either core change or exposure change can realize frontier escape at fixed depth, for exact and randomized stages\. Appendix[B\.3](https://arxiv.org/html/2610.10611#A2.SS3)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](https://arxiv.org/html/2610.10611#A2.SS4)extends the construction to finite chains\.

## 6Depth limits and certificate substitution

###### Theorem 6\.1\(Conditional depth obstructions\)\.

Fixk≥1k\\geq 1\.

1. \(i\)IfΣk𝖯≠Σk\+1𝖯\\Sigma\_\{k\}^\{\\mathsf\{P\}\}\\neq\\Sigma\_\{k\+1\}^\{\\mathsf\{P\}\}, there is a taskRRand an exact depth\-\(k\+1\)\(k\+1\)stageTTwhose native language is not contained in the frontier of any sound exact depth\-kkstage forRR\.
2. \(ii\)The analogous assertion holds for randomized depthsk,k\+1k,k\+1ifΣk𝖱𝖵≠Σk\+1𝖱𝖵\\Sigma\_\{k\}^\{\\mathsf\{RV\}\}\\neq\\Sigma\_\{k\+1\}^\{\\mathsf\{RV\}\}\.
3. \(iii\)IfΣk\+1𝖯≠Σk\+2𝖯\\Sigma\_\{k\+1\}^\{\\mathsf\{P\}\}\\neq\\Sigma\_\{k\+2\}^\{\\mathsf\{P\}\}, some exact depth\-\(k\+2\)\(k\+2\)target cannot be covered by any sound randomized depth\-kkstage for its task\.

The proof is in Appendix[A\.5](https://arxiv.org/html/2610.10611#A1.SS5)\.

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 depthkkcannot 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\)\.

LetV⁡\(x,a,u\)V\(x,a,u\)be polynomial\-time with bounded stringsa,ua,u, and letG⁡\(x,a\)G\(x,a\)be a deterministic polynomial\-time guard for the supported family\. Suppose a polynomial\-time exact checkerC⁡\(x,a,π\)C\(x,a,\\pi\)has polynomially bounded certificates and, for every bounded\(x,a\)\(x,a\)withG⁡\(x,a\)=1G\(x,a\)=1, satisfies

∃πC\(x,a,π\)=1⟺∀uV\(x,a,u\)=1\.\\exists\\pi\\ C\(x,a,\\pi\)=1\\quad\\Longleftrightarrow\\quad\\forall u\\ V\(x,a,u\)=1\.Then the guarded language

\{x:∃a\[G\(x,a\)∧∀uV\(x,a,u\)=1\]\}\\displaystyle\\\{x:\\exists a\\ \[G\(x,a\)\\wedge\\forall u\\ V\(x,a,u\)=1\]\\\}=\{x:∃a,π\[G\(x,a\)∧C\(x,a,π\)=1\]\}\\displaystyle\\qquad=\\\{x:\\exists a,\\pi\\ \[G\(x,a\)\\wedge C\(x,a,\\pi\)=1\]\\\}has an exact depth\-one certificate representation\. Soundness ofCCalone gives containment, not equality\. If this guarded language isΣ2𝖯\\Sigma\_\{2\}^\{\\mathsf\{P\}\}\-complete, such a uniform sound\-and\-complete certificate system impliesΣ2𝖯=𝖭𝖯\\Sigma\_\{2\}^\{\\mathsf\{P\}\}=\\mathsf\{NP\}\.

The proof is in Appendix[A\.5](https://arxiv.org/html/2610.10611#A1.SS5)\.

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𝔽2\\mathbb\{F\}\_\{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\.

## 7A reproducible audit, from exact to probabilistic

### 7\.1Running task and three exact designs

Letx⋆x\_\{\\star\}be the task of repairing a lookup function on the three\-element array\(alpha,beta,gamma\)\(\\texttt\{alpha\},\\texttt\{beta\},\\texttt\{gamma\}\)\. The declared input domain for testing isI=\{−3,−2,−1,0,1,2,3,4\}I=\\\{\-3,\-2,\-1,0,1,2,3,4\\\}\. Correct behavior returns the indexed element for0≤i<30\\leq i<3and 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\_\{\\star\},z\)\\iff\\forall i\\in I,\\quad z\(i\)=\\mathrm\{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 ati=−1i=\-1returnsgammarather 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 forRR: deterministic testing does not imply exact verification of a broader specification\.

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⋆\}\.\\mathrm\{L\}\_\{R\}\(S\_\{\\rm cert\}\)=\\varnothing,\\qquad\\mathrm\{F\}\_\{R\}\(S\_\{\\rm cert\}\)=\\\{x\_\{\\star\}\\\}\.The exhaustive stage exposes the valid repair natively and has both languages equal to\{x⋆\}\\\{x\_\{\\star\}\\\}\. 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\_\{\\star\}\\\}\.S2S\_\{2\}makes that record native, so both languages are\{x⋆\}\\\{x\_\{\\star\}\\\}\. ThusS0→S1S\_\{0\}\\to S\_\{1\}expands support and the frontier, andS1→S2S\_\{1\}\\to S\_\{2\}internalizes already permitted support\. The directS0→S2S\_\{0\}\\to S\_\{2\}comparison exhibits native escape under unchanged authority\. Repeating default attempts inS1S\_\{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\.2A controlled stochastic extension

For the same finite checkerCC, reject malformed and out\-of\-bound records deterministically\. On well\-formed bounded tuples, define a noisy terminal core that uses two fair bits: with probability3/43/4it returnsCCand with probability1/41/4it returns1−C1\-C\. Accepted exact tuples now have probability3/43/4and rejected tuples probability1/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 to27/3227/32and5/325/32without 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 probability1−\(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\.3A growing family with an enforced interface

Consider synthesizing a straight\-line XOR program forfa​\(u\)=⨁j=1daj​ujf\_\{a\}\(u\)=\\bigoplus\_\{j=1\}^\{d\}a\_\{j\}u\_\{j\}, givenx=\(1d,a\)x=\(1^\{d\},a\)witha∈𝔽2da\\in\\mathbb\{F\}\_\{2\}^\{d\}\. A candidate is a sorted listzzof distinct variable indices and computesfz​\(u\)=⨁j∈zujf\_\{z\}\(u\)=\\bigoplus\_\{j\\in z\}u\_\{j\}; the empty list returns zero\. Correctness meansfz​\(u\)=fa​\(u\)f\_\{z\}\(u\)=f\_\{a\}\(u\)for everyu∈𝔽2du\\in\\mathbb\{F\}\_\{2\}^\{d\}\. The exact core compares coefficient vectors and binds the output to the program recorded in the transcripttt\. 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 quotaq∈\{0,…,B⁡\(d\)\}q\\in\\\{0,\\ldots,B\(d\)\\\}, defaulting tob0​\(d\)b\_\{0\}\(d\), and

ExpB,b0​\(x,q,t\)⇔0≤q≤B⁡\(d\),t​is a canonical program,\|t\|≤q\.\\mathrm\{Exp\}\_\{B,b\_\{0\}\}\(x,q,t\)\\iff 0\\leq q\\leq B\(d\),\\quad t\\text\{ is a canonical program\},\\quad\|t\|\\leq q\.Here\|t\|\|t\|counts references; its binary encoding has lengthO⁡\(d​log⁡d\)O\(d\\log d\)\. Assume0≤b0​\(d\)≤B⁡\(d\)≤d0\\leq b\_\{0\}\(d\)\\leq B\(d\)\\leq 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\)\}\.\\mathrm\{L\}\_\{R\}\(S\_\{B,b\_\{0\}\}\)=\\\{\(1^\{d\},a\):\\\|a\\\|\_\{0\}\\leq b\_\{0\}\(d\)\\\},\\qquad\\mathrm\{F\}\_\{R\}\(S\_\{B,b\_\{0\}\}\)=\\\{\(1^\{d\},a\):\\\|a\\\|\_\{0\}\\leq 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\}\\leq q\\leq B\(d\), the ratio is2d−1\+1/22^\{d\-1\}\+1/2\. Ifq<‖a‖0q<\\\|a\\\|\_\{0\}, both probabilities are zero\. Forb=⌊d/2⌋b=\\lfloor d/2\\rfloor, 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 everyd≥1d\\geq 1, witnessed by anyaaof weightb\+1b\+1\.

The proof, including exclusion of all old witnesses, is in Appendix[A\.7](https://arxiv.org/html/2610.10611#A1.SS7)\.

An existential accepted\-input language does not record the probability of finding its witnesses\. For the policy comparison, a uniformdd\-bit mask proposes each program with probability2−d2^\{\-d\}\. A second policy uses the directly computed correct program with probability1/21/2and that uniform proposal otherwise\. At a quota admitting the correct program, their per\-attempt success probabilities are2−d2^\{\-d\}and1/2\+2−\(d\+1\)1/2\+2^\{\-\(d\+1\)\}\. Both retain full proposal support; disallowed proposals are rejected by the harness\. ForMMindependent attempts with per\-attempt successpp, success is1−\(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𝖯\\mathsf\{P\}\. A budget that is only advisory supplies no such exclusion proof\. The reference implementation enumerates all target vectors, candidate programs, and quotas for1≤d≤61\\leq d\\leq 6, tests malformed and forged records, and checks the formulas using exact arithmetic\. Atd=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](https://arxiv.org/html/2610.10611#S7.F4)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 atd=6d=6Target weight‖a‖0\\\|a\\\|\_\{0\}\(\|L\|,\|F\|\)\(\|L\|,\|F\|\)00112233445566Source \(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\)NNNN–––Expanded \(B,b0\)=\(4,4\)\(B,b\_\{0\}\)=\(4,4\)\(57,57\)\(57,57\)NNNNN––Number oftargets1615201561N: native O: optional only –: blocked

1248163264000\.250\.250\.50\.50\.750\.7511Proposal attemptsMMAt least one success\(b\) Search with the same quotaUniform: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 quotaq=3q=3and targeta=\(1,1,1,0,0,0\)a=\(1,1,1,0,0,0\); under default quota zero both have success probability zero\. ForMMindependent attempts the curves are1−\(1−p\)M1\-\(1\-p\)^\{M\}\. The solution mixture computes the correct program with probability1/21/2and 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](https://arxiv.org/html/2610.10611#S7.Thmtheorem1)\.This example proves Proposition[7\.1](https://arxiv.org/html/2610.10611#S7.Thmtheorem1)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](https://arxiv.org/html/2610.10611#S8.Thmtheorem1)and the conditional selection bound in Proposition[8\.2](https://arxiv.org/html/2610.10611#S8.Thmtheorem2)are separate theorems with separate premises\.

### 7\.4Declaration protocol and disagreement rules

A reproducible audit first records the following evidence, before assigning complexity labels or claiming an escape\.

1. 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. 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. 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. 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. 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𝒜S\\mathcal\{A\}\_\{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](https://arxiv.org/html/2610.10611#S5.Thmtheorem3)\. Appendix[C](https://arxiv.org/html/2610.10611#A3)specifies how to reproduce the artifacts\. We do not use the names of commercial systems or multiagent roles to assign establishedΣk𝖯\\Sigma\_\{k\}^\{\\mathsf\{P\}\}orΣk𝖱𝖵\\Sigma\_\{k\}^\{\\mathsf\{RV\}\}membership to their implementations\.

## 8Recursive 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](https://arxiv.org/html/2610.10611#bib.bib1)\]\. 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\.1What 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](https://arxiv.org/html/2610.10611#bib.bib21),[23](https://arxiv.org/html/2610.10611#bib.bib23),[22](https://arxiv.org/html/2610.10611#bib.bib22)\]\. RSIAgent accumulates memory without parameter updates and freezes it for subsequent evaluation\[[14](https://arxiv.org/html/2610.10611#bib.bib14)\]\. 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](https://arxiv.org/html/2610.10611#bib.bib12),[20](https://arxiv.org/html/2610.10611#bib.bib20),[26](https://arxiv.org/html/2610.10611#bib.bib26)\]\. 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](https://arxiv.org/html/2610.10611#bib.bib18),[19](https://arxiv.org/html/2610.10611#bib.bib19)\]\. AIDE2reports 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](https://arxiv.org/html/2610.10611#bib.bib13)\]\.

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](https://arxiv.org/html/2610.10611#A4)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](https://arxiv.org/html/2610.10611#bib.bib1)\]\.

### 8\.2Deployed 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\),\\widehat\{S\}\_\{i\+1\}=U\_\{i\}\(S\_\{i\},h\_\{i\};\\eta\_\{i\}\),\\qquad S\_\{i\+1\}=J\_\{i\}\(S\_\{i\},\\widehat\{S\}\_\{i\+1\},h\_\{i\}\),whereUiU\_\{i\}is an improver,hih\_\{i\}is its bounded interaction history,ηi\\eta\_\{i\}is its proposal randomness, andJiJ\_\{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 relationRRused to evaluate deployed outputs must also be distinguished from the improvement criterion used byJiJ\_\{i\}\. A higher benchmark score is neither a proof ofLR​\(Si\)⊆LR​\(Si\+1\)\\mathrm\{L\}\_\{R\}\(S\_\{i\}\)\\subseteq\\mathrm\{L\}\_\{R\}\(S\_\{i\+1\}\)nor an escape witness\.

Figure[5](https://arxiv.org/html/2610.10611#S8.F5)separates the update loop from the two contracts used to analyze it: accepted\-language structure and false\-selection risk\.

DeployedSiS\_\{i\}ImproverUiU\_\{i\}CandidateS^i\+1\\widehat\{S\}\_\{i\+1\}SelectionJiJ\_\{i\}Next deployedSi\+1S\_\{i\+1\}historyhih\_\{i\},proposal coinsηi\\eta\_\{i\}select candidateor retainSiS\_\{i\}Accepted changes can affect later improvement roundsStructural contractJointly uniformA,E,CA,E,C; common bounds andkkLenv∈Σk𝖱𝖵L\_\{\\rm env\}\\in\\Sigma\_\{k\}^\{\\mathsf\{RV\}\}Gap and task soundness for every admitted candidateSelection contractPr⁡\(Bi∣ℋi−1\)≤δi\\Pr\(B\_\{i\}\\mid\\mathcal\{H\}\_\{i\-1\}\)\\leq\\delta\_\{i\}Pr⁡\(⋃i=1MBi\)≤∑i=1Mδi\\Pr\(\\bigcup\_\{i=1\}^\{M\}B\_\{i\}\)\\leq\\sum\_\{i=1\}^\{M\}\\delta\_\{i\}Conditional validity for every selection callCount every selection call, including rejectionsFigure 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](https://arxiv.org/html/2610.10611#S8.Thmtheorem1)’s fixed admission, exposure, interpretation, and common bounds, admitted histories define a language in the same verification class\. Proposition[8\.2](https://arxiv.org/html/2610.10611#S8.Thmtheorem2)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\)\.

Leth,ch,cbe polynomially bounded history and candidate strings\. Assume one deterministic polynomial\-time admission predicateA⁡\(x,h,c\)A\(x,h,c\), one such exposure predicateE⁡\(x,h,c,σ,t\)E\(x,h,c,\\sigma,t\), and one uniform polynomial\-time randomized terminal interpreterC⁡\(x,h,c,z,t,y→,r\)C\(x,h,c,z,t,\\vec\{y\};r\)\. These algorithms include all encoding and object\-domain checks\. There are common polynomial object, coin, and runtime bounds and the same fixedkkmove 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 candidateSh,cS\_\{h,c\}satisfies the pointwise gap and quantified soundness for a commonRR\. Chooseh,ch,cbefore the moves and hidden coins\. Then

Lenv=\{x:∃h,c\[A\(x,h,c\)∧x∈FR\(Sh,c\)\]\}∈Σk𝖱𝖵\.L\_\{\\rm env\}=\\\{x:\\exists h,c\\ \[A\(x,h,c\)\\wedge x\\in\\mathrm\{F\}\_\{R\}\(S\_\{h,c\}\)\]\\\}\\in\\Sigma\_\{k\}^\{\\mathsf\{RV\}\}\.The same holds with native reach in place of the frontier\. With exact terminal checks both languages belong toΣk𝖯\\Sigma\_\{k\}^\{\\mathsf\{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](https://arxiv.org/html/2610.10611#A1.SS6)\.

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 deployedSiS\_\{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](https://arxiv.org/html/2610.10611#S8.T2)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\.

Table 2:A concrete update contract\. All quota languages here remain in𝖯\\mathsf\{P\}; these edits are not claims of learned recursive improvement\.
### 8\.3Selection 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](https://arxiv.org/html/2610.10611#bib.bib24)\]\. 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](https://arxiv.org/html/2610.10611#bib.bib25)\]\. 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\. LetBiB\_\{i\}be the event that theiith selection call accepts a candidate that violates a separately specified improvement criterion\. Letℋi−1\\mathcal\{H\}\_\{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 mostMMselection calls, including rejected candidates\. If for every reachable pre\-call history

Pr⁡\(Bi∣ℋi−1\)≤δi\\Pr\(B\_\{i\}\\mid\\mathcal\{H\}\_\{i\-1\}\)\\leq\\delta\_\{i\}for fixed nonnegative budgetsδi\\delta\_\{i\}, then

Pr⁡\(⋃i=1MBi\)≤∑i=1Mδi\.\\Pr\\\!\\left\(\\bigcup\_\{i=1\}^\{M\}B\_\{i\}\\right\)\\leq\\sum\_\{i=1\}^\{M\}\\delta\_\{i\}\.In particular, if each invalid fixed candidate has per\-trial false acceptance probability at most1/31/3, evaluated with independent fresh coins after the candidate is fixed, an odd majority sizeN≥18​log⁡\(M/δ\)N\\geq 18\\log\(M/\\delta\)gives a total false\-selection probability at mostδ\\deltafor0<δ<10<\\delta<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](https://arxiv.org/html/2610.10611#A1.SS6)\.

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](https://arxiv.org/html/2610.10611#bib.bib17)\]\. The finite audit’s three\-call example gives the concrete risk: three independent opportunities to accept a fixed invalid candidate with probability1/41/4each yield probability37/6437/64of 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\.

## 9Verifier scope, related work, and limitations

### 9\.1A realizable bounded\-error contract

The pointwise condition is restrictive but has concrete algorithmic instances\. Consider checkingA​B=CAB=Cfor suppliedn×nn\\times nmatrices over𝔽2\\mathbb\{F\}\_\{2\}\. Draw a uniformv∈𝔽2nv\\in\\mathbb\{F\}\_\{2\}^\{n\}and accept ifA⁡\(B​v\)=C​vA\(Bv\)=Cv, repeating twice independently and requiring both tests to pass\. This is the standard randomized matrix\-product check\[[6](https://arxiv.org/html/2610.10611#bib.bib6)\]\. Correct products pass with probability one; incorrect products pass both independent tests with probability at most1/41/4\. Thus the gap and task soundness hold uniformly\. The row argument is in Appendix[A\.8](https://arxiv.org/html/2610.10611#A1.SS8)\. 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\.2Related work

Bounded alternation and the polynomial hierarchy supply the deterministic background\[[2](https://arxiv.org/html/2610.10611#bib.bib2)\]\. Arthur–Merlin systems distinguish when verifier coins are visible to a witness\[[5](https://arxiv.org/html/2610.10611#bib.bib5)\]; our hidden\-terminal\-coin, pointwise\-gap model is a particular restricted semantics\. The classical randomized hierarchy bound supplies the sandwich proof\[[3](https://arxiv.org/html/2610.10611#bib.bib3),[4](https://arxiv.org/html/2610.10611#bib.bib4)\]\. 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](https://arxiv.org/html/2610.10611#bib.bib7)\]\. 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](https://arxiv.org/html/2610.10611#bib.bib8)\]\. Reflexion uses feedback and episodic memory to improve subsequent trials without weight updates\[[9](https://arxiv.org/html/2610.10611#bib.bib9)\]\. 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](https://arxiv.org/html/2610.10611#bib.bib10)\], and studies of intrinsic self\-correction identify limits without external feedback\[[11](https://arxiv.org/html/2610.10611#bib.bib11)\]\. 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](https://arxiv.org/html/2610.10611#bib.bib27)\]\. This motivates recording the location of a failure rather than treating additional agents as evidence of stronger verification\.

### 9\.3Limitations

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𝖬𝖠\\mathsf\{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\.

## 10Conclusion

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](https://arxiv.org/html/2610.10611#A3)\.

## 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](https://arxiv.org/abs/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](https://doi.org/10.1145/322234.322243)\.
- \[3\]M\. Sipser\. A complexity theoretic approach to randomness\. In*STOC*, pp\. 330–335, 1983\.[doi:10\.1145/800061\.808762](https://doi.org/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](https://doi.org/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](https://doi.org/10.1016/0022-0000(88)90028-1)\.
- \[6\]R\. Freivalds\. Fast probabilistic algorithms\. In*Mathematical Foundations of Computer Science 1979*, LNCS 74, pp\. 57–69\. Springer, 1979\.[doi:10\.1007/3\-540\-09526\-8\_5](https://doi.org/10.1007/3-540-09526-8_5)\.
- \[7\]G\. Irving, P\. Christiano, and D\. Amodei\. AI safety via debate\. 2018\.[arXiv:1805\.00899](https://arxiv.org/abs/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](https://arxiv.org/abs/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](https://arxiv.org/abs/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](https://arxiv.org/abs/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](https://arxiv.org/abs/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](https://arxiv.org/abs/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](https://arxiv.org/abs/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](https://arxiv.org/abs/2609.15364v2)\.
- \[15\]Google DeepMind\. AlphaEvolve: How our Gemini\-powered coding agent is scaling impact across fields\. May 7, 2026\.[Google DeepMind research update](https://deepmind.google/blog/alphaevolve-impact/)\.
- \[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](https://doi.org/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*, pp\. 117–126, 2015\.[arXiv:1411\.2664](https://arxiv.org/abs/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](https://arxiv.org/abs/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](https://arxiv.org/abs/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](https://arxiv.org/abs/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](https://arxiv.org/abs/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](https://arxiv.org/abs/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](https://arxiv.org/abs/2510.04618v3)\.
- \[24\]X\. Fu, A\. Kulanthaivelu, and Y\. Yamada\. Self improvement via fast tree\-search\. September 17, 2026\.[arXiv:2609\.19526v1](https://arxiv.org/abs/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](https://arxiv.org/abs/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](https://arxiv.org/abs/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](https://arxiv.org/abs/2503.13657v3)\.

## Appendix AProofs of the main results

The notation and assumptions are those of Sections[2](https://arxiv.org/html/2610.10611#S2)–[3](https://arxiv.org/html/2610.10611#S3)\. 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\.1Stage languages and deterministic recovery

###### Proof of Proposition[3\.4](https://arxiv.org/html/2610.10611#S3.Thmtheorem4)\.

Default support is among the permitted supports, yielding the first inclusion; soundness yields the second\. For frontier membership, guessσ,t,z\\sigma,t,zin the leading existential block withy1y\_\{1\}, check exposure, and use the predicateExpS∧CoreS\\mathrm\{Exp\}\_\{S\}\\wedge\\mathrm\{Core\}\_\{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\\sigma=\\sigma\_\{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](https://arxiv.org/html/2610.10611#S3.Thmtheorem5)\.

Choose pointwise\-gap verifiersV0,V1V\_\{0\},V\_\{1\}for the two languages, padding their move and coin lengths to common polynomial bounds and ignoring padding\. SetR⁡\(x,z\)⇔z=1∧x∈L1R\(x,z\)\\iff z=1\\wedge x\\in L\_\{1\}\. Default support exposes tagt=0t=0; one optional support exposest=1t=1\. On outputz=1z=1and transcript tagt=it=i, the core runsViV\_\{i\}; it rejects other encodings\. Native acceptance givesL0L\_\{0\}, and optional support givesL0∪L1=L1L\_\{0\}\\cup L\_\{1\}=L\_\{1\}\. Soundness follows from the inclusion of languages\. DeterministicViV\_\{i\}give the exact construction\. ∎

### A\.2False acceptance and majority amplification

###### Proof of Proposition[4\.1](https://arxiv.org/html/2610.10611#S4.Thmtheorem1)\.

Choose a proper languageL∈𝖭𝖯L\\in\\mathsf\{NP\}with certificate predicateV⁡\(x,y\)V\(x,y\)and setR⁡\(x,z\)⇔z=1∧x∈LR\(x,z\)\\iff z=1\\wedge x\\in L\. Expose onlyt=εt=\\varepsilon\. Forz=1z=1, let the core accept ifV⁡\(x,y\)=1V\(x,y\)=1orr=0n\+2r=0^\{n\+2\}\. All other encodings are rejected\. Each tuple accepts with probability either11or2−\(n\+2\)≤1/42^\{\-\(n\+2\)\}\\leq 1/4, so the gap holds\. Bounded\-error acceptance has frontier exactlyLL, while an existential lucky tape accepts every input\. ∎

###### Proof of Theorem[4\.2](https://arxiv.org/html/2610.10611#S4.Thmtheorem2)\.

LetgN​\(p\)g\_\{N\}\(p\)be the probability that an odd majority accepts when each trial accepts with probabilitypp\. ForN=2​m\+1N=2m\+1, direct binomial expansion gives

g2​m\+3​\(p\)−g2​m\+1​\(p\)=\(2​m\+1m\)​pm\+1​\(1−p\)m\+1​\(2​p−1\)\.g\_\{2m\+3\}\(p\)\-g\_\{2m\+1\}\(p\)=\\binom\{2m\+1\}\{m\}p^\{m\+1\}\(1\-p\)^\{m\+1\}\(2p\-1\)\.ConsequentlygN​\(p\)≥pg\_\{N\}\(p\)\\geq pforp≥1/2p\\geq 1/2andgN​\(p\)≤pg\_\{N\}\(p\)\\leq pforp≤1/2p\\leq 1/2\. In particular, the high and low sides of the gap remain on their respective sides for every oddNN, includingN=1N=1\. The standard independent Bernoulli tail bound\[[16](https://arxiv.org/html/2610.10611#bib.bib16)\]gives error at mostexp\(−2N\(1/6\)2\)=e−N/18\\exp\(\-2N\(1/6\)^\{2\}\)=e^\{\-N/18\}\. ThusDS\[N\]=DSD\_\{S^\{\[N\]\}\}=D\_\{S\}pointwise\. Applying the same quantifiers and exposure predicates proves every claimed semantic equality and preserves task soundness\. ∎

### A\.3Hierarchy bounds and derandomization

###### Proof of Theorem[4\.3](https://arxiv.org/html/2610.10611#S4.Thmtheorem3)\.

The first inclusions use zero coins\. For the upper bound, the total thresholded matrixD⁡\(x,y→\)D\(x,\\vec\{y\}\)is in𝖡𝖯𝖯\\mathsf\{BPP\}\. If the last block is existential, substitute its classicalΣ2𝖯\\Sigma\_\{2\}^\{\\mathsf\{P\}\}representation∃u​∀v​B\\exists u\\forall v\\,B; if universal, substitute itsΠ2𝖯\\Pi\_\{2\}^\{\\mathsf\{P\}\}representation∀u​∃v​B′\\forall u\\exists v\\,B^\{\\prime\}\. Merging adjacent blocks of the same type leavesk\+1k\+1blocks\. The universal\-start argument is identical with the initial quantifier reversed\. ∎

###### Proof of Theorem[4\.4](https://arxiv.org/html/2610.10611#S4.Thmtheorem4)\.

For \(i\), chooseL∈Σ1𝖱𝖵∖𝖭𝖯L\\in\\Sigma\_\{1\}^\{\\mathsf\{RV\}\}\\setminus\\mathsf\{NP\}and use Theorem[3\.5](https://arxiv.org/html/2610.10611#S3.Thmtheorem5)withL0=L1=LL\_\{0\}=L\_\{1\}=L\. Exact depth\-one frontiers belong to𝖭𝖯\\mathsf\{NP\}by Proposition[3\.4](https://arxiv.org/html/2610.10611#S3.Thmtheorem4)and cannot equalLL\. For \(ii\),DSD\_\{S\}is a single uniform𝖡𝖯𝖯\\mathsf\{BPP\}language on the encoded tuple\. Under𝖡𝖯𝖯=𝖯\\mathsf\{BPP\}=\\mathsf\{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\.4Guard\-transfer invariance

###### Proof of Proposition[5\.2](https://arxiv.org/html/2610.10611#S5.Thmtheorem2)\.

Guarding the core multiplies its acceptance probability byg∈\{0,1\}g\\in\\\{0,1\\\}, so it preserves the gap and changes the threshold matrix tog∧DSg\\wedge 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,\\sigma,z,t,\\vec\{y\}\)=\\mathrm\{Exp\}\_\{S\}\(x,\\sigma,t\)\\wedge D\_\{S\}\(x,z,t,\\vec\{y\}\)\.Quantifying it with default or existential support recovers native or frontier membership\. ∎

### A\.5Depth obstructions and certificate substitution

###### Proof of Theorem[6\.1](https://arxiv.org/html/2610.10611#S6.Thmtheorem1)\.

For \(i\) chooseL∈Σk\+1𝖯∖Σk𝖯L\\in\\Sigma\_\{k\+1\}^\{\\mathsf\{P\}\}\\setminus\\Sigma\_\{k\}^\{\\mathsf\{P\}\}, setRL​\(x,z\)⇔z=1∧x∈LR\_\{L\}\(x,z\)\\iff z=1\\wedge x\\in L, and realize native reachLLby the exact case of Theorem[3\.5](https://arxiv.org/html/2610.10611#S3.Thmtheorem5)\. Every sound exact depth\-kksource hasFRL​\(S\)∈Σk𝖯\\mathrm\{F\}\_\{R\_\{L\}\}\(S\)\\in\\Sigma\_\{k\}^\{\\mathsf\{P\}\}andFRL​\(S\)⊆L\\mathrm\{F\}\_\{R\_\{L\}\}\(S\)\\subseteq L\. If its frontier coveredLL, the two sets would be equal, contradicting the choice ofLL\. For \(ii\), 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 \(iii\), chooseL∈Σk\+2𝖯∖Σk\+1𝖯L\\in\\Sigma\_\{k\+2\}^\{\\mathsf\{P\}\}\\setminus\\Sigma\_\{k\+1\}^\{\\mathsf\{P\}\}and an exact target with native reachLL\. Randomized source frontiers lie inΣk\+1𝖯\\Sigma\_\{k\+1\}^\{\\mathsf\{P\}\}by Theorem[4\.3](https://arxiv.org/html/2610.10611#S4.Thmtheorem3); soundness again forces containment inLL\. Coverage would force the forbidden equality\. ∎

###### Proof of Proposition[6\.2](https://arxiv.org/html/2610.10611#S6.Thmtheorem2)\.

Retain the polynomial\-time guardGG, substitute the certificate equivalence only whereG=1G=1, and mergea,πa,\\piinto one existential block\. The resulting language is in𝖭𝖯\\mathsf\{NP\}\. AΣ2𝖯\\Sigma\_\{2\}^\{\\mathsf\{P\}\}\-complete language in𝖭𝖯\\mathsf\{NP\}puts all ofΣ2𝖯\\Sigma\_\{2\}^\{\\mathsf\{P\}\}in𝖭𝖯\\mathsf\{NP\}under polynomial reductions; the opposite inclusion is standard\. With soundness alone only the forward implication from certified to universal acceptance is available\. ∎

### A\.6Bounded self\-modification and adaptive selection

###### Proof of Proposition[8\.1](https://arxiv.org/html/2610.10611#S8.Thmtheorem1)\.

Includeh,c,σ,t,zh,c,\\sigma,t,zwith 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,\\sigma,t,z,\\vec\{y\};r\)=A\(x,h,c\)\\wedge E\(x,h,c,\\sigma,t\)\\wedge C\(x,h,c,z,t,\\vec\{y\};r\)\.Each conjunct is interpreted by its single uniform algorithm, including the declared domain checks; the predicatesA,EA,Eprecede and do not depend on the verification moves\. Invalid records reject with probability one\. Valid records inherit the candidate’s gap, soVVis a total polynomial\-time randomized predicate with the required gap\. Move\-independent deterministic guards commute with the nonempty quantifier domains\. Thus quantifyingVVrecognizes exactlyLenvL\_\{\\rm env\}without adding a block\. For the native union, substitute the uniformly computed default support forσ\\sigma\. Quantified soundness of every admitted candidate makes the enclosing language sound forRR\. Without coins the same construction has a deterministic matrix\. ∎

###### Proof of Proposition[8\.2](https://arxiv.org/html/2610.10611#S8.Thmtheorem2)\.

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](https://arxiv.org/html/2610.10611#bib.bib16)\]bounds each call’s majority error bye−N/18≤δ/Me^\{\-N/18\}\\leq\\delta/M, as in Theorem[4\.2](https://arxiv.org/html/2610.10611#S4.Thmtheorem2)\. Sum over the calls\. ∎

#### Countable selection budgets\.

For a countable sequence, budgetsδi=δ/2i\\delta\_\{i\}=\\delta/2^\{i\}still give total error at mostδ\\deltaunder the same conditional premise\. This probability statement does not imply a uniform polynomial runtime for an infinite run\.

### A\.7The quota\-enforced XOR family

###### Proof of Proposition[7\.1](https://arxiv.org/html/2610.10611#S7.Thmtheorem1)\.

For eachjj, evaluating on the basis vectoreje\_\{j\}shows that a correct canonical program includes indexjjif and only ifaj=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𝔽2\\mathbb\{F\}\_\{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\. UsingO⁡\(d​log⁡d\)O\(d\\log 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 mostb0​\(d\)b\_\{0\}\(d\), and some allowed support admits it precisely when its length is at mostB⁡\(d\)B\(d\)\. This proves the two language formulas\. For a target of weightb\+1b\+1, every source\-exposed transcript has at mostbbreferences, 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 are2−d2^\{\-d\}and1/2\+2−\(d\+1\)1/2\+2^\{\-\(d\+1\)\}, whose ratio is2d−1\+1/22^\{d\-1\}\+1/2\. Takingddarbitrarily large proves the unbounded ratio without changing either language\. Below the correct program’s quota both success probabilities are zero\. Independence ofMMattempts gives1−\(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\)\\binom\{d\}\{j\}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](https://arxiv.org/html/2610.10611#S8.Thmtheorem1)\. The example isolates these obligations without claiming to explain how a learned improver discovers a useful policy\.

### A\.8The randomized matrix\-product check

For the checker in Section[9](https://arxiv.org/html/2610.10611#S9), correct products pass every test\. IfA​B≠CAB\\neq C, choose a nonzero rowddofA​B−CAB\-C\. The dot productd​vdvis a uniform bit for uniformv∈𝔽2nv\\in\\mathbb\{F\}\_\{2\}^\{n\}, soPr⁡\(d​v=0\)=1/2\\Pr\(dv=0\)=1/2\. Acceptance impliesd​v=0dv=0, giving a one\-test false\-acceptance probability at most1/21/2\. Independent repetitions therefore both accept with probability at most1/41/4\. The same bound holds for every incorrect matrix triple, establishing the pointwise gap and task soundness claimed in the main text\.

## Appendix BRepresentation machinery and supporting constructions

### B\.1Simulation and support normalization

###### Definition B\.1\(Simulation\)\.

WriteS⪯simTS\\preceq^\{\\rm sim\}Twhen the depths agree and a polynomial\-time mapϕ⁡\(x,t\)\\phi\(x,t\)mapsNatS​\(x\)\\mathrm\{Nat\}\_\{S\}\(x\)intoNatT​\(x\)\\mathrm\{Nat\}\_\{T\}\(x\)andExpS∗​\(x\)\\mathrm\{Exp\}\_\{S\}^\{\*\}\(x\)intoExpT∗​\(x\)\\mathrm\{Exp\}\_\{T\}^\{\*\}\(x\), and preserves accepted\-input membership on each mapped transcript fromSStoTT\.

###### 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ϕ\\phiand apply the preserved acceptance condition; mutual simulation gives both inclusions\. For normalization, default support exposes⟨0,t⟩\\langle 0,t\\rangleprecisely whenttwas native, and optional support exposes⟨1,σ,t⟩\\langle 1,\\sigma,t\\rangleprecisely whenExpS​\(x,σ,t\)\\mathrm\{Exp\}\_\{S\}\(x,\\sigma,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 samett\. Existential acceptance needs only this surjectivity, giving equality of both languages\. ∎

### B\.2The local invariant of guard transfer

###### Proposition B\.3\(Local guard invariant\)\.

At a fixed tuple, every observationh⁡\(e,d\)h\(e,d\)of exposure and thresholded acceptance that is invariant under Boolean guard transfer factors uniquely throughe∧de\\wedge d\.

###### Proof\.

Invariance meansh⁡\(e∧g,d\)=h⁡\(e,g∧d\)h\(e\\wedge g,d\)=h\(e,g\\wedge d\)\. Sete=1e=1andg=e′g=e^\{\\prime\}to obtainh⁡\(e′,d\)=h⁡\(1,e′∧d\)h\(e^\{\\prime\},d\)=h\(1,e^\{\\prime\}\\wedge d\)\. Thush⁡\(e,d\)=f⁡\(e∧d\)h\(e,d\)=f\(e\\wedge d\)forf⁡\(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\.3Separate same\-depth escape constructions

###### Proposition B\.4\(Two independent same\-depth realizations\)\.

For anyL0⊊L1L\_\{0\}\\subsetneq L\_\{1\}inΣk𝖱𝖵\\Sigma\_\{k\}^\{\\mathsf\{RV\}\}, frontier escape can be realized at depthkkby changing only the core, or by changing only exposure\.

###### Proof\.

UseR⁡\(x,z\)⇔z=1∧x∈L1R\(x,z\)\\iff z=1\\wedge x\\in L\_\{1\}and verifiersV0,V1V\_\{0\},V\_\{1\}\. All constructed cores reject outputs other thanz=1z=1\. For a core\-only change, both stages expose onlyt=εt=\\varepsilonand useV0,V1V\_\{0\},V\_\{1\}respectively\. For an exposure\-only change, fix one core that usesViV\_\{i\}on tagiion*all*transcripts, including unexposed ones\. The source exposes only tag00under every support state; the target exposes both tags already under default support\. Thus the source frontier isL0L\_\{0\}, target native reach isL1L\_\{1\}, and the core is unchanged even on the newly exposed tag\. ∎

The deterministic version follows with exact verifiers\.

### B\.4Finite chains of same\-depth frontier expansion

###### Proposition B\.5\.

Given a finite chainL0⊊⋯⊊LmL\_\{0\}\\subsetneq\\cdots\\subsetneq L\_\{m\}inΣk𝖱𝖵\\Sigma\_\{k\}^\{\\mathsf\{RV\}\}and any sequence of labelsbi∈\{core,support\}b\_\{i\}\\in\\\{\\mathrm\{core\},\\mathrm\{support\}\\\}, there are sound depth\-kkstages with native and frontier languages both equal toLiL\_\{i\}such that transitioniichanges only the component indicated bybib\_\{i\}\.

###### Proof\.

SetR⁡\(x,z\)⇔z=1∧x∈LmR\(x,z\)\\iff z=1\\wedge x\\in L\_\{m\}and choose a pointwise\-gap verifierViV\_\{i\}for eachLiL\_\{i\}, with common padded bounds\. Initially expose one active tag usingV0V\_\{0\}\. Every core rejectsz≠1z\\neq 1\. For every future support transitionii, prepare a distinct dormant tag whose core already usesVi\+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 byVi\+1V\_\{i\+1\}; leave all dormant tags unchanged\. At stepi\+1i\+1, old active languages lie inLi\+1L\_\{i\+1\}and either one new active tag or every active tag realizesLi\+1L\_\{i\+1\}\. Thus the union is exactlyLi\+1L\_\{i\+1\}\. Soundness holds because even dormant languages lie withinLmL\_\{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 CFinite 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 inanc/\. The ancillary artifact version is2026\-10\-07\-arxiv\. ItsMANIFEST\.jsonrecords 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\. Fromanc/,python3 reproduce\.pyruns the regressions and compares regenerated results with the saved records\. PDF compilation separately requires a LaTeX distribution with the packages declared in the rootmain\.tex\.

The vector figures are supplied as TikZ/PGFPlots source infigures/at the package root\. Their three numeric tables are generated byanc/integrated/figures/generate\_data\.pyusing 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\.

Fromanc/, the exact regressions run as follows:

```
python3 -m unittest discover -s code/exact_audit -p ’test_*.py’ -v
```

The self\-contained additional artifact isintegrated/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 all2×22\\times 2Boolean 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](https://arxiv.org/html/2610.10611#A1.SS8); it does not replace that proof\.

From the sameanc/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 ford≤4d\\leq 4, check malformed and mismatched records, and verify actual transcript inclusion for internalization\. Its JSON report records exact language counts and proposal probabilities ford≤6d\\leq 6, with the policy target, selected stage, default and optional quotas, and attempt count explicitly recorded\. The escape witness is a separate target\. Atd=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 usesexposure\_atom\_inclusionfor fact sets andnative\_to\_frontier\_transcript\_inclusionfor the exposure premise of Theorem[5\.3](https://arxiv.org/html/2610.10611#S5.Thmtheorem3); 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 DSelf\-improvement mechanisms and comparative evidence

The mechanisms in Table[3](https://arxiv.org/html/2610.10611#A4.T3)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 lineReported mechanismStage comparison and evidence neededAutonomy and inherited improvementDuan et al\. organize RSI by control over execution, strategy, experience, deployment adaptation, and inherited improvement mechanisms\. They separate structural from effective recursion\[[1](https://arxiv.org/html/2610.10611#bib.bib1)\]\.An autonomy level does not determinekk\. 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 adaptationGEPA reflects on execution traces to evolve prompts; ACE incrementally maintains playbooks; RSIAgent carries frozen memory into evaluation\[[21](https://arxiv.org/html/2610.10611#bib.bib21),[23](https://arxiv.org/html/2610.10611#bib.bib23),[14](https://arxiv.org/html/2610.10611#bib.bib14)\]\.Declare which context was already available through optional support\. Compare memory admissibility and use under matched task and output contracts\.Workflow searchAFlow uses Monte Carlo tree search over code\-represented workflows and execution feedback\[[22](https://arxiv.org/html/2610.10611#bib.bib22)\]\.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 codeDGM retains an archive of self\-modified agents\. AHE exposes editable components and records predicted effects; Self\-Harness validates proposed edits with regression tests\[[12](https://arxiv.org/html/2610.10611#bib.bib12),[20](https://arxiv.org/html/2610.10611#bib.bib20),[26](https://arxiv.org/html/2610.10611#bib.bib26)\]\.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 improversSTOP optimizes the improver’s own program\. Hyperagents jointly exposes task and meta\-agent code to modification\. AIDE2explores research\-agent improvement across successive versions\[[18](https://arxiv.org/html/2610.10611#bib.bib18),[19](https://arxiv.org/html/2610.10611#bib.bib19),[13](https://arxiv.org/html/2610.10611#bib.bib13)\]\.VersionSiS\_\{i\},UiU\_\{i\}, andJiJ\_\{i\}separately\. Measure the updated improver on common starting agents and budgets, and identify any fixed outer search or evaluation process\.Search evaluationSIFT aggregates pairwise judge preferences through a Bradley–Terry model to guide parent selection and evaluation priority\[[24](https://arxiv.org/html/2610.10611#bib.bib24)\]\.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 designAI4AI\-Bench uses ten research repositories and reruns candidate training algorithms from scratch under a hidden fixed evaluator\[[25](https://arxiv.org/html/2610.10611#bib.bib25)\]\.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 discoveryAlphaEvolve uses executable evaluation to guide program search and reports applications across scientific domains\[[15](https://arxiv.org/html/2610.10611#bib.bib15)\]\.Declare the candidate language and correctness objective\. Distinguish a better discovered program from a change to the agent that discovers programs\.### D\.1Comparing task improvement and improver improvement

The RSI survey’s Headroom\-Closed Index summarizes benchmark scores; its post\-2026 extension is explicitly illustrative\[[1](https://arxiv.org/html/2610.10611#bib.bib1)\]\. 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@kkmetric\. In that comparison the meta agent is held fixed, and the best child is selected using validation performance before test performance is measured\[[19](https://arxiv.org/html/2610.10611#bib.bib19)\]\. 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](https://arxiv.org/html/2610.10611#S7.SS4)\.

### D\.2Separating diagnosis, ranking, and acceptance

AHE reports that its predicted fixes are more informative than its predicted regressions, with many regressions remaining unforeseen\[[20](https://arxiv.org/html/2610.10611#bib.bib20)\]\. SIFT explicitly treats its judge as an intermediate ranking signal rather than a certificate of downstream superiority\[[24](https://arxiv.org/html/2610.10611#bib.bib24)\]\. 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](https://arxiv.org/html/2610.10611#bib.bib26)\]\.

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](https://arxiv.org/html/2610.10611#bib.bib25)\], help specify an experimental comparison; they do not by themselves establish a uniform mathematical soundness contract\. This is why Proposition[8\.2](https://arxiv.org/html/2610.10611#S8.Thmtheorem2)states a conditional\-error premise instead of inferring one from benchmark scores\.