Paper deep dive
Counterfactual Regret for Reflective Agents with Lean-Verified Guarantees
Zhongnian Li, Shi Xu, Mengting Xu, Peng Ying, Xinzheng Xu
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Reflective language agents reuse feedback and memory to adapt across tasks without updating model weights. However, existing guarantees for policy selection and action generation do not by themselves establish when local reflection yields long-term performance guarantees for the complete agent under resource constraints. In this paper, we address this gap by deriving sufficient conditions for sublinear counterfactual regret from local generation and deployment guarantees, while retaining the native controller. Specifically, we establish a resource-sensitive transfer that bounds full-state deployment discrepancies along actual execution paths and preserves the own-history laws of both learner and comparator. Besides, local generation reliability yields a cumulative generation opportunity bound, linking policy acquisition to long-term performance through an explicit quality, coverage, and hard-budget tradeoff. To verify these guarantees, we formalize the conditional proof chain for all thirteen numbered theoretical results in Lean, including a native instance with repeated policy growth and imperfect validation.
Tags
Links
- Source: https://arxiv.org/abs/2610.14790v1
- Canonical: https://arxiv.org/abs/2610.14790v1
Trouble viewing inline? Open PDF directly →
Full Text
187,860 characters extracted from source content.
Expand or collapse full text
Counterfactual Regret for Reflective Agents with Lean-Verified Guarantees Zhongnian Li Shi Xu Mengting Xu Peng Ying Xinzheng Xu †thanks: Corresponding author: xxzheng@cumt.edu.cn Affiliation: School of Computer Science and Technology / School of Artificial Intelligence Affiliation: China University of Mining and Technology Affiliation: Xuzhou, China Email: zhongnianli,xushi,mengtingxu,pengying,xxzheng@cumt.edu.cn Abstract Reflective language agents reuse feedback and memory to adapt across tasks without updating model weights. However, existing guarantees for policy selection and action generation do not by themselves establish when local reflection yields long-term performance guarantees for the complete agent under resource constraints. In this paper, we address this gap by deriving sufficient conditions for sublinear counterfactual regret from local generation and deployment guarantees, while retaining the native controller. Specifically, we establish a resource-sensitive transfer that bounds full-state deployment discrepancies along actual execution paths and preserves the own-history laws of both learner and comparator. Besides, local generation reliability yields a cumulative generation opportunity bound, linking policy acquisition to long-term performance through an explicit quality, coverage, and hard-budget tradeoff. To verify these guarantees, we formalize the conditional proof chain for all thirteen numbered theoretical results in Lean, including a native instance with repeated policy growth and imperfect validation. The complete Lean proof artifacts are available in an anonymous repository11 1 https://github.com/subeidiyixiaoqianfeng/counterfactual-regret-lean-proofs for verification and reproduction. 1 Introduction Reflective language agents use feedback to revise decisions and retain experience for subsequent tasks. With frozen model weights, linguistic reflection and memory provide a practical means of adaptation during execution. Reflexion and Self-Refine demonstrate benefits in coding, reasoning, and iterative task solving (Shinn et al., 2023; Madaan et al., 2023). Reusable instructions can carry lessons from earlier outcomes into later decisions, making reflection valuable for systems that must adapt through interaction. These capabilities motivate understanding how local feedback-driven changes contribute to long-term agent performance. However, existing guarantees for policy selection and action generation do not by themselves establish sustained performance gains for the complete reflective process. With frozen model weights, useful reflection must produce reusable policies and influence subsequent execution within available resources. These effects are coupled because current decisions shape future feedback and policy availability. Understanding this coupling requires explicit conditions linking local adaptation to long-term performance. We study this gap through counterfactual regret against resource-feasible procedures on their own histories, following the policy-regret comparison principle (Arora et al., 2012). Rather than requiring every reflection to improve performance, we identify generation and deployment conditions under which average excess loss vanishes while retaining the native controller. Contributions. We develop a conditional theory connecting local reflection mechanisms to a complete native-agent regret guarantee. Theorem 11 retains the native controller and identifies conditions for sublinear regret through three contributions. 1. Resource-sensitive native transfer. Full-state deployment discrepancies are bounded along actual resource paths, preserving both counterfactual marginals and connecting hard budgets to cumulative loss. 2. Locally derived generation bounds. Local reliability connects policy acquisition to long-term performance, with an explicit quality, coverage and hard-budget tradeoff. 3. A Lean-verified conditional proof chain. All thirteen numbered results are formalized, including a concrete native instance that derives compatible interfaces and a sublinear bound from its mechanisms. Related work. Growing-expert tracking provides guarantees for expanding pools (Mourtada and Maillard, 2017), while generative action sets jointly optimize creation and selection through a context-conditioned oracle and quadratic mismatch model (Xu et al., 2026). We connect local generation reliability to complete reflective executions through a generation opportunity bound. Its composition with deployment stability captures how obtaining useful policies and executing them jointly affect regret. Policy regret formalizes action-responsive comparisons (Arora et al., 2012), with recent Markov-game guarantees under function-approximation conditions (Nguyen-Tang and Arora, 2025). We develop a resource-sensitive transfer for a retained native controller. Full-state perturbations accumulate along actual execution paths, with hard budgets controlling their cumulative effect. The construction preserves both native marginals while connecting local deployment conditions to own-history regret. Merten et al. (2018) established Coq-verified multiplicative weights and composed distributed-system guarantees. Our Lean development connects growing selection, local generation reliability, deployment stability, and completed-task correspondence through explicit interfaces, supporting reproducible checking of the composed no-regret guarantee. 2 Model and reference algorithm We define the complete reflective execution before introducing a reference process whose selection guarantee can be transferred to it. 2.1 Histories, policies, and counterfactual regret Use task indices t=0,…,T−1t=0,…,T-1, internal-operation indices s≥0s≥ 0, and reference-slot indices r=0,…,Rr=0,…,R. These clocks differ. All logarithms are natural, E1\E\ is the indicator of event E, and ⟨u,v⟩=∑iu(i)v(i) u,v = _iu(i)v(i). Appendix K collects notation and its Lean correspondence. Definition 1 (Legal history and operations). Fix measurable operation and result spaces , U, O, an initial-history set ℋ0opH op_0, and a measurable admissibility relation (h,u,o) E(h,u,o). Define ℋs+1op=h∥(u,o)∣h∈ℋsop,(h,u,o)H op_s+1=\h \|(u,o) h op_s,\ E(h,u,o)\ and ℋop=⨆s≥0ℋsopH op= _s≥ 0H op_s, assuming each level measurable. Here ∥\| appends a completed operation and result. A measurable legal-operation set (h) U(h) restricts the next control. Histories record contexts, primitive actions, structured outcomes, memory, versioned registrations, and resource counters. Execution can name only an already registered executable identity. Legal prefixes need not have positive probability. Hard budgets impose equation 2. A history records what has happened. An execution policy specifies the distribution of the next primitive action, given the current context and memory. Definition 2 (Execution policy and card identity). Let ,, X, M, A be measurable context, memory, and primitive-action spaces. Identity i names an immutable card program and interpreter version, inducing a probability kernel πi(da∣x,m) _i(da x,m) on A. For every measurable D⊆D A, πi(D∣x,m) _i(D x,m) is measurable in (x,m)(x,m), and πi(∣x,m)=1 _i( A x,m)=1. Selecting i chooses a kernel, whereas sampling a executes an action. Memory changes may alter its output law without changing identity. Program or interpreter changes require a new identity. A meta-policy governs the complete procedure, including when to create cards and which existing card to execute. It is therefore more than a selector over a fixed library. Definition 3 (Meta-policy and own-history law). A meta-policy μ(du∣h)μ(du h) is a measurable probability kernel on operations with μ((h)∣h)=1μ( U(h) h)=1. Generation, validation, memory updates, and execution are distinct operations. The history index allows time-dependent control. Composing this kernel with environment and runtime kernels, assuming internal operations terminate, induces task records Zt∈tZ_t _t. Here Z0Z_0 is the prescribed initial record and Zt+1Z_t+1 completes task t. The task history is Ht=(Z0,…,Zt)∈ℋttask=∏u=0tuH_t=(Z_0,…,Z_t) _t task= _u=0^tZ_u. Its recursively generated law is ℙμP_μ. A nonempty class ℳM contains complete procedures, not distributions over current cards. The native learner A is another procedure and need not belong to ℳM. The native controller is the operation-selection kernel μA(du∣h) _A(du h) of procedure A, with μA((h)∣h)=1 _A( U(h) h)=1. Operation-result, environment, and runtime kernels additionally determine ℙAP_A. Retaining this controller means that it need not execute the reference algorithm. Decisions may change across histories, and transfer conditions do not hold automatically. Fix a common measurable loss scorer σt _t on ℋt+1taskH_t+1 task and set Yt=σt(Ht+1)∈[0,1]Y_t= _t(H_t+1)∈[0,1], with smaller values preferred. This scalar evaluates the structured output, rather than replacing it. Define LTA=∑t<TYtA,JT(A)=ℙALTA,RT(A,ℳ)=JT(A)−infμ∈ℳJT(μ).L_T^A= _t<TY_t^A, J_T(A)=E_P_AL_T^A, R_T(A,M)=J_T(A)- _μ J_T(μ). (1) The expectation includes environment, generation, validation, runtime, logging, and private control randomness present in the specified execution. A deterministic environment is permitted. The native model may respond causally to past actions. Oblivious loss tables are required only in the benchmark of Section 4. For a measurable trajectory map rAr_A and source law Γ , ((rA)#Γ)(D)=Γ(rA−1(D))((r_A)_\# )(D)= (r_A^-1(D)) for every measurable event D. The subscript #\# denotes measure pushforward, so (rA)#Γ=ℙA(r_A)_\# =P_A fixes the native trajectory law. Proposition 4 (Well-defined native objective). The loss in equation 1 is measurable and integrable, with 0≤JT(A)≤T0≤ J_T(A)≤ T. A measurable realization rAr_A on a coupling space with (rA)#Γ=ℙA(r_A)_\# =P_A satisfies Γ[LTA∘rA]=JT(A)E_ [L_T^A r_A]=J_T(A). Proposition 4 preserves the full native trajectory law, not merely the current action distribution. This is required for every comparator. The counterfactual is a complete execution. Both procedures use the same environment mechanism and scoring function, but supply their own preceding actions and memories to that mechanism. Equal initial conditions do not mean equal subsequent observations. Randomness may be coupled only with the correct marginals. In particular, the comparator cannot use a card solely because the learner generated it. The class restriction is fixed before taking the infimum. This is the distinction between comparison on a realized loss sequence and policy-regret comparison in a responsive system (Arora et al., 2012; Anava et al., 2015). 2.2 Resource constraints and interfaces Require a nonempty comparator class satisfying, under each own law, ℙμCosttμ≤Bt for every t=0,…,T=1.P_μ\Cost_t^μ≤ B_t for every t=0,…,T\=1. (2) Here CosttμCost_t^μ is cumulative resource use after t completed tasks, including failed internal attempts, and BtB_t is a deterministic prefix budget. Any additional operationwise limit belongs to (h) U(h). Hard feasibility restricts procedures, not task loss. Mean feasibility instead bounds ℙμCosttμE_P_μCost_t^μ, assuming integrability, and is not equivalent to equation 2. The resource interface determines admissible procedures. The representation interface maps a comparator to a causal execution-card path and charges any lost advantage. The deployment interface compares that represented execution with what the native runtime actually does. These maps need not commute. For example, compilation may consume resources, and imperfect implementation may change future memory. We therefore impose them in a specified order and account for adjacent differences, rather than treating them as independent interchangeable assumptions. 2.3 Growing-library exponential weights The reference algorithm is a mathematical comparison process, not an installed controller. Write ℱr−F_r^- for completed pre-draw information, with realization hrh_r. The nonempty finite identity set ℐr=ℐr(hr)I_r=I_r(h_r) and sampling law are measurable with respect to this information. Let w0=ν0w_0= _0 be a probability distribution and Θr _r a nonnegative row-stochastic transition from ℐrI_r to ℐr+1I_r+1. For nonnegative estimated losses ℓ^r(i) _r(i) and learning rate η>0η>0, define pr(i)=wr(i)∑jwr(j),wr+1(j)=∑iwr(i)e−ηℓ^r(i)Θr(i,j).p_r(i)= w_r(i) _jw_r(j), w_r+1(j)= _iw_r(i)e^-η _r(i) _r(i,j). (3) This recurrence uses the EXP3 and Fixed-Share primitives (Auer et al., 2002; Herbster and Warmuth, 1998; Cesa-Bianchi and Lugosi, 2006). Its normalizers are positive. For persistent identity labels, Fixed Share uses Θr(i,j)=(1−α)i=j+ανr+1(j),0<α<1, _r(i,j)=(1-α)1\i=j\+α _r+1(j), 0<α<1, (4) where νr+1 _r+1 has full support and persistent labels share one immutable namespace. With a full-support initial prior, this specialization gives positive draw probabilities, including for newborn cards. A positive normalizer alone does not imply coordinatewise support. Generation is not optimized by this recurrence. Algorithm 1 Growing-Library Exponential Weights 1. Slot cap N=R+1N=R+1, η>0η>0, prior ν0 _0, and admissible run protocol 2. Accepted-score interface supplying Mr,yr,qrM_r,y_r,q_r and positive sampling support 3. Initialize registered identities ℐ0I_0 and weights w0←ν0w_0← _0. 4. for r=0,…,N−1r=0,…,N-1 do 5. if slot r is active according to completed history hrh_r then 6. Set pr(i)←wr(i)/∑jwr(j)p_r(i)← w_r(i)/ _jw_r(j) and sample Jr∼prJ_r p_r. 7. Execute the admissible scored run and receive the selected outcome OrO_r. 8. Set ℓ^r _r by equation 6 and settle task and resource costs. 9. else 10. Set ℓ^r←0 _r← 0 and apply the terminal convention of Section 2.4. 11. end if 12. Form ℐr+1I_r+1 from completed registrations and choose row-stochastic Θr _r. 13. Set wr+1(j)←∑i∈ℐrwr(i)e−ηℓ^r(i)Θr(i,j)w_r+1(j)← _i _rw_r(i)e^-η _r(i) _r(i,j). 14. end for The protocol supplies lawful run boundaries and acceptance probabilities, not unexecuted losses. A valid arrival closes a scored slot before the next draw. New identities enter only after generation and validation, and can be selected at that next draw. There is no additional draw outside the loop. The terminal weight update is for analysis, not another task. The synchronized run contract in Section 2.4 remains essential. 2.4 Feedback model and selection guarantee At fixed hrh_r, let kr(i,o)k_r(i,o) be the finite outcome law under reference execution of identity i, and let λr(i,o) _r(i,o) be its prescribed task-loss total. The target ℓrref(i)=∑okr(i,o)λr(i,o) ^ref_r(i)= _ok_r(i,o) _r(i,o) is defined by that execution, not by accepted logs. Let Mr(i,o)∈0,1M_r(i,o)∈\0,1\ mark acceptance and yr(i,o)∈[0,dr]y_r(i,o)∈[0,d_r] be the proxy score, with predictable cap drd_r. Suppressing hrh_r, require qr(i)=∑okr(i,o)Mr(i,o)>0,∑okr(i,o)Mr(i,o)yr(i,o)=qr(i)ℓrref(i).q_r(i)= _ok_r(i,o)M_r(i,o)>0, _ok_r(i,o)M_r(i,o)y_r(i,o)=q_r(i) ^ref_r(i). (5) It is stronger than positive logging probability. It excludes selection-biased accepted scores unless an additional correction is proved. The estimator is ℓ^r(i)=Jr=iMr(Jr,Or)yr(Jr,Or)pr(i)qr(i). _r(i)= 1\J_r=i\M_r(J_r,O_r)y_r(J_r,O_r)p_r(i)q_r(i). (6) Only the executed observation enters the update. A structured outcome is compatible with equation 5, because its score is a measurable function. The scalar score does not replace the full state used by reflection. Covered stopping rules. Fix a deterministic cap N=R+1N=R+1. The event r activer active means that the reference process has not terminated and completed history hrh_r authorizes slot r. Its indicator r active1\r active\ is 11 on this event and 00 otherwise, determined in ℱr−F_r^- before the current draw. This is distinct from card availability ℐrI_r and feedback acceptance MrM_r. Inactive slots produce an absorbing terminal token and zero targets and estimates. A result may stop later slots, never retroactively cancel its own slot. Held-run length and eligibility require the synchronized accepted-score contract. Arbitrary current-draw-dependent aggregation needs an additional bridge, not merely a shared clock. Lemma 5 (Local and stopped observation moments). In a finite observation model satisfying equation 5, with positive pr(i)p_r(i), the conditional draw–outcome law gives Jr,Or|hrℓ^r(i)=ℓrref(i),Jr,Or|hr⟨pr,ℓ^r2⟩≤dr2∑i∈ℐr1qr(i).E_J_r,O_r h_r _r(i)= ^ref_r(i), _J_r,O_r h_r p_r, _r^2 ≤ d_r^2 _i _r 1q_r(i). (7) For a predictable comparator coordinate vr(hr)v_r(h_r), let er=⟨pr,ℓ^r⟩−ℓ^r(vr)−ℓrref(Jr)+ℓrref(vr)e_r= p_r, _r - _r(v_r)- ^ref_r(J_r)+ ^ref_r(v_r). Under the recursively generated bounded stopped law ℙstopP_ stop, ℙstop∑r<Nr activeer _P_ stop _r<N1\r active\e_r =0, =0, (8) ℙstop∑r<Nr active⟨pr,ℓ^r2⟩ _P_ stop _r<N1\r active\ p_r, _r^2 ≤∑r<Nℙstop(r)[r activedr2∑iqr(i)−1]. ≤ _r<NE_P_ stop^(r) [1\r active\d_r^2 _iq_r(i)^-1 ]. (9) Here ℙstop(r)P_ stop^(r) is the actual completed-prefix law, not a distribution obtained by revealing the stopping time in advance. From the potential to expected selection regret. A reference experiment supplies equation 3 and its integrable moments on one coupling Γμ _μ. For a supported predictable path =μ=(v0,…,vR)v=v^μ=(v_0,…,v_R) with vr∈ℐrv_r _r, define C()=−logν0(v0)−∑r<RlogΘr(vr,vr+1).C(v)=- _0(v_0)- _r<R _r(v_r,v_r+1). (10) Require C()≤C(v)≤ C on every modeled path, with deterministic C, and the deterministic second-moment budget ∑r=0RΓμ[∑i∈ℐrpr(i)ℓ^r(i)2]≤Vest. _r=0^RE_ _μ\! [ _i _rp_r(i) _r(i)^2 ]≤ V_ est. (11) This is a raw second moment, not a centered variance. The coupling must induce the same pre-draw law as the observation interface. Path support alone does not ensure predictability. Theorem 6 (Growing selection). Under these conditions, ∑r=0RΓμ[ℓrref(Jr)−ℓrref(vr)]≤Cη+ηVest2. _r=0^RE_ _μ[ ^ref_r(J_r)- ^ref_r(v_r)]≤ Cη+ η V_ est2. (12) Theorem 6 balances path complexity C against feedback uncertainty VestV_ est through η. Its potential proof uses Lemma 5, with the observation interface and recurrence sharing the same pre-draw law. Equality of isolated identity marginals is insufficient. No-regret behavior is derived when these terms grow slowly enough. 3 Counterfactual regret guarantees We first decompose regret, then bound deployment and generation effects locally. This order identifies which discrepancies each theorem controls. 3.1 Regret decomposition and transfer Fix μ and a coupling Γμ _μ preserving both native laws. Every endpoint below is an expected total at fixed horizon T, whose subscript is suppressed. In particular, Jsel=∑r=0RΓμℓrref(Jr)J^sel= _r=0^RE_ _μ ^ref_r(J_r) and Jμav=∑r=0RΓμℓrref(vr)J_μ^av= _r=0^RE_ _μ ^ref_r(v_r), whereas JAnat=JT(A)J_A^nat=J_T(A) and Jμnat=JT(μ)J_μ^nat=J_T(μ). Specify intermediate score random variables and integrate them under this same coupling. The resulting certificates are JAnat−JAref J_A^nat-J_A^ref ≤EA, ≤ E_A, JAref−Jsel J_A^ref-J^sel ≤F+b+DA, ≤ F+P_b+D_A, (13) Jμav−Jμal J_μ^av-J_μ^al ≤G, ≤ G, Jμal−Jμcl J_μ^al-J_μ^cl ≤bS, ≤ bS, Jμcl−Jμpath J_μ^cl-J_μ^path ≤hresp(S+1)+DC, ≤ h_resp(S+1)+D_C, Jμpath−Jμref J_μ^path-J_μ^ref ≤Enf, ≤ E_ nf, Jμref−Jμnat J_μ^ref-J_μ^nat ≤EC, ≤ E_C, Vest V_ est ≤bV, ≤ bV, where b=hresp(⌈T/b⌉+Nb+1)P_b=h_resp( T/b +N_b+1). The integers b≥1b≥ 1 and Nb,S,hresp≥0N_b,S,h_resp≥ 0 are the nominal run cap, extra-boundary envelope, path switch bound, and response scale. A certificate here is an explicit bound such as equation 13, assumed at an interface or derived from local conditions, not an empirical validation. The response scale is not an automatic mixing time. The deterministic V bounds scaled second-moment capacity, not a Bellman value. The learner reference score is JArefJ_A^ref. The available substitute has score JμavJ_μ^av. The score JμalJ_μ^al evaluates the ideal represented comparator path after alignment to run starts, on clean reference slots. The score JμclJ_μ^cl removes run alignment, JμpathJ_μ^path removes the reference response discrepancy, and JμrefJ_μ^ref is the reference meta-policy endpoint after undoing representation, before native deployment. These names specify the order of the comparison. Each endpoint must be defined before a certificate is asserted. F charges displaced foreground task opportunities. bP_b charges clean-prefix loss due to at most NbN_b extra boundaries. DA,DCD_A,D_C are score-calibration allowances. G charges policies missing from the available library. S bounds represented path changes. EnfE_ nf charges the loss of advantage under representation. EA,ECE_A,E_C charge implementation differences. Hard resource costs constrain admissibility separately. A birth is not automatically both a displaced task and a unit task penalty. Theorem 7 (Conditional native counterfactual transfer). Let ℳM be nonempty. Suppose every μ∈ℳμ has a compatible reference experiment, own-law endpoint realizations, and certificates equation 13 with common budgets, C, and η>0η>0. Put Δ=EA+F+DA+G+DC+Enf+EC =E_A+F+D_A+G+D_C+E_ nf+E_C. Then RT(A,ℳ)≤UT=Δ+Cη+ηbV2+hresp(⌈T/b⌉+Nb+1)+bS+hresp(S+1).R_T(A,M)≤ U_T= + Cη+ η bV2+h_resp( T/b +N_b+1)+bS+h_resp(S+1). (14) Theorem 7 transfers a reference selection bound by accounting for each adjacent discrepancy once. The native learner need not execute Fixed Share, but complete-execution identities must be justified. Comparator couplings may differ while preserving the same learner law. Unrelated logs do not establish this correspondence. Corollary 8 (Conditional no regret). Along a positive-horizon family, all budgets, b,Nb,S,hresp,C,V,ηb,N_b,S,h_resp,C,V,η may depend on T but are uniform over μ at that horizon. If each of the five normalized terms ΔT,C/η+ηbV/2T,hresp(⌈T/b⌉+Nb+1)T,bST,hresp(S+1)T T, C/η+η bV/2T, h_resp( T/b +N_b+1)T, bST, h_resp(S+1)T (15) tends to zero, then max0,RT(A,ℳ)/T→0 \0,R_T(A,M)/T\→ 0. This is upper no regret, not convergence of signed regret to zero. For fixed hresp>0h_resp>0 and fixed b, the third term has limit at least hresp/b>0h_resp/b>0. Thus fixed run caps do not automatically give sublinearity. Appendix K illustrates compatible horizon scalings. 3.2 Resource-sensitive deployment stability Mean-preserving rounding need not preserve nonlinear reflection, so we compare full-state transition kernels. Here StS_t ranges over a time-varying finite type containing all behavior-relevant memory, card-library, resource, and runtime components. Use common initial law pinitp init and scores ct(St)∈[0,1]c_t(S_t)∈[0,1]. An update affects the next state, not the score already produced at boundary t. These are state-score positions. Appendix L proves the completed-task padding with T+1T+1 positions for T tasks and zero terminal resource, preserving both boundary scores. Let KtK_t be a native kernel and LtL_t its feedback-processed reference. Define JT(K)=ℙK∑t<Tct(St)J_T(K)=E_P_K _t<Tc_t(S_t). Assume TV(Kt(s,⋅),Lt(s,⋅))=12∑j|Kt(s,j)−Lt(s,j)|≤εt(s).TV(K_t(s,·),L_t(s,·))= 12 _j|K_t(s,j)-L_t(s,j)|≤ _t(s). (16) For each remaining horizon n with t+1+n≤Tt+1+n≤ T, let Vt+1,nLV^L_t+1,n be its expected accumulated score. Whenever εt(s)>0 _t(s)>0, assume its range over next states is contained in an interval of length ht(s)≥0h_t(s)≥ 0. At zero-error states no such range hypothesis is needed. Theorem 9 (Local stability on the actual native path). The preceding local conditions imply |JT(K)−JT(L)|≤ℙK∑t<Tht(St)εt(St).|J_T(K)-J_T(L)| _P_K _t<Th_t(S_t) _t(S_t). (17) For nonnegative H¯,ε¯,χt(s),rt(s) H, , _t(s),r_t(s), assume ht(s)≤H¯h_t(s)≤ H, εt(s)≤ε¯χt(s) _t(s)≤ \, _t(s), and cminχt(s)≤rt(s)c_ _t(s)≤ r_t(s) for cmin>0c_ >0. If every positive-probability native path has ∑t<Trt(St)≤BT _t<Tr_t(S_t)≤ B_T, then |JT(K)−JT(L)|≤H¯ε¯BT/cmin.|J_T(K)-J_T(L)|≤ H B_T/c_ . (18) Alternatively, without a bounded-influence assumption, a uniform local TV bound εt(s)≤ε¯T _t(s)≤ _T gives |JT(K)−JT(L)|≤T2ε¯T|J_T(K)-J_T(L)|≤ T^2 _T. Theorem 9 weights each local shift by its downstream sensitivity along the actual law. Appendix J explains its role in joint resource design. Theorem 10 (Resource-sensitive native transfer). Suppose Theorem 7 applies to the reference endpoints LA,LμL_A,L_μ, with completed-task scores connected by Appendix L. Apply the local resource contract of Theorem 9 to KA,LAK_A,L_A and uniformly to Kμ,LμK_μ,L_μ, with budgets BA,BCB_A,B_C and common H¯,ε¯,cmin H, ,c_ . Then JT(KA)−infμJT(Kμ)≤UT+H¯ε¯cmin(BA+BC).J_T(K_A)- _μJ_T(K_μ)≤ U_T+ H c_ (B_A+B_C). (19) For fixed H¯ε¯/cmin H /c_ , UT=o(T)U_T=o(T) and BA+BC=o(T)B_A+B_C=o(T) imply upper no regret. The alternative local-only bound is sublinear if Tε¯T→0T _T→ 0 on both endpoints. Theorem 10 restores both native endpoints, hence the two resource budgets. These outer connections must not duplicate implementation allowances already comparing the same endpoints in equation 13. 3.3 Generation reliability and the main guarantee Theorem 10 can be instantiated without assuming that the total generation gap is small. We call the following joint success and quality requirements local generation reliability. Fix each comparator before play. Decompose its available-to-aligned gap into finitely many causal generation episodes. In episode e, a normalized finite kernel generates trial outcomes using previous trial history. A Boolean analysis predicate identifies a validated and retained comparator-suitable outcome. On every still-unsuccessful history, its next-trial probability is at least ρe∈(0,1] _e∈(0,1]. The algorithm need not know which card is optimal. This is a conditional coverage assumption, not an oracle input or an independence assumption. After kek_e trials, let ξe∈0,1 _e∈\0,1\ indicate that none succeeded under its actual episode law ℙeP_e. There are τe _e delay tasks and nen_e post-generation tasks. On each completed generation history, require the conditional expected per-task available-minus-aligned gap to be at most 11 during delay and at most δe+ξe _e+ _e afterwards, with δe≥0 _e≥ 0. The successful card must support a causal available path satisfying this local quality condition. A useful text that is discarded or inaccessible is not a success. The episode sums must equal the actual generation endpoint difference, without counting the same task twice. Theorem 11 (Native guarantee from local conditions). Write gTgen(μ)=Jμav−Jμalg_T gen(μ)=J_μ^av-J_μ^al. Under these episode conditions, uniformly for the specified comparator class, gTgen(μ)≤∑eτe+ne[δe+(1−ρe)ke].g_T gen(μ)≤ _e\ _e+n_e[ _e+(1- _e)^k_e]\. (20) For nonnegative envelopes, if ∑eτe≤AT _e _e≤ A_T, ∑ene≤T _en_e≤ T, δe≤δT _e≤ _T, and (1−ρe)ke≤fT(1- _e)^k_e≤ f_T, the right side is at most AT+T(δT+fT)A_T+T( _T+f_T). Keep the other reference certificates, use identity deployment arrows inside the reference transfer, and impose the full-state local resource contracts on the two outer native-to-reference arrows. Use the validated completed-task instance and padded stability clock of Appendix L. With UTrestU_T rest denoting equation 14 with G=EA=EC=0G=E_A=E_C=0, this gives RT≤UTrest+AT+T(δT+fT)+κ(BA+BC),κ=H¯ε¯/cmin.R_T≤ U_T rest+A_T+T( _T+f_T)+κ(B_A+B_C), κ= H /c_ . (21) For a positive-horizon family with fixed ρ∈(0,1]ρ∈(0,1] and κ, suppose fT=(1−ρ)kTf_T=(1-ρ)^k_T, kT→∞k_T→∞, δT→0 _T→ 0, and UTrest,AT,BA+BC=o(T)U_T rest,A_T,B_A+B_C=o(T). Then max0,RT/T→0 \0,R_T/T\→ 0. A concrete native instance. Appendix I constructs a native verified-template reflector satisfying the interfaces jointly. Appendix N extends the instance evidence to repeated growth with imperfect validation and persistent selection errors. Corollary 12 (Native verified-template reflection). For each integer k≥1k≥ 1, the constructed instance has T=k2+kT=k^2+k tasks, hard budget 2k+22k+2, and own-history comparator class ℳ0M_0 containing immediate repair and no reflection. Then RT(Ak,ℳ0)≤(2+log2)k+k22−k+14≤(3+log2)k+14.R_T(A_k,M_0)≤(2+ 2)k+k^22^-k+ 14≤(3+ 2)k+ 14. (22) Positive normalized regret vanishes along this family, whereas no reflection has regret T. Corollary 13 (Quality and hard-budget tradeoff). Fix a causal design satisfying the episode conditions and remaining interfaces of Theorem 7, uniformly over hard-feasible comparators. At tolerance δe≥0 _e≥ 0 and coverage ρe(δe)∈(0,1] _e( _e)∈(0,1], let ce(δe)≥0c_e( _e)≥ 0 bound prepaid trial cost including failures, kek_e bound prefix counts, and BTother≥0B_T other≥ 0 bound other costs. Put U¯T=UTrest+EA+EC U_T=U_T rest+E_A+E_C. If equation 23 holds, the learner is hard-feasible and satisfies equation 24, where BTother+∑ekece(δe) B_T other+ _ek_ec_e( _e) ≤BT, ≤ B_T, (23) RT R_T ≤U¯T+∑eτe+ne[δe+e−keρe(δe)]. ≤ U_T+ _e \ _e+n_e [ _e+e^-k_e _e( _e) ] \. (24) For a positive-horizon family, if ∑ene≤T _en_e≤ T, δe≤δT→0 _e≤ _T→ 0, keρe(δe)≥λT→∞k_e _e( _e)≥ _T→∞, and U¯T+∑eτe=o(T) U_T+ _e _e=o(T), then max0,RT/T→0 \0,R_T/T\→ 0. Appendix J gives feasible quotas and compatibility with Corollary 12, charging delay and deployment once. 4 Near-matching bounds under paid growth 4.1 The paid-growth model This theoretical benchmark isolates paid public growth and sparse feedback. It is not an empirical evaluation or a lower bound for every native interface. There are m≥1m≥ 1 public phases of n≥1n≥ 1 primitive rounds, with T=mnT=mn and integer registration budget B≥4mB≥ 4m. A public registration schedule releases a strictly growing library. With zero-based phase index j<mj<m, set Kj=⌈B/2⌉+⌊(j+1)⌊B/2⌋m⌋.K_j= B/2 + (j+1) B/2 m . (25) Each registration costs one unit, the total is B, and all intermediate prefixes are hard-feasible. Old identities persist, unborn identities are illegal, and the schedule is public. Put j(t)=⌊t/n⌋j(t)= t/n and [K]0=0,…,K−1[K]_0=\0,…,K-1\. The legal table domain is =(t,i)∣0≤t<T,i∈[Kj(t)]0D=\(t,i) 0≤ t<T,\ i∈[K_j(t)]_0\. An oblivious table ℓ∈0,1 ∈\0,1\^D has entries ℓtbase(i) _t base(i). The learner emits It∈[Kj(t)]0I_t∈[K_j(t)]_0. Only its selected bit is observed, independently erased with probability 1−q1-q, where 0<q≤10<q≤ 1. Task loss is Yt=12(ℓtbase(It)+t>0,It≠It−1).Y_t= 12 ( base_t(I_t)+1\t>0,\ I_t≠ I_t-1\ ). (26) The comparator path class is =∏j=0m−1[Kj]0V= _j=0^m-1[K_j]_0. For ∈v , define It=vj(t)I_t^v=v_j(t) and LT(,ℓ)L_T(v, ) by summing equation 26 with It=ItI_t=I_t^v. Thus both sides pay actual switches, the first draw is free, and registration is not charged again. Let A contain all causal randomized phase controllers, using all previously visible phase and primitive history. Define ℛbin∗(T,m,B,q)=infA∈supℓ∈0,1ℙA,ℓ,q∑t<TYt−min∈LT(,ℓ),R^*_ bin(T,m,B,q)= _A∈ A _ ∈\0,1\^D \E_P_A, ,q _t<TY_t- _v L_T(v, ) \, (27) The law ℙA,ℓ,qP_A, ,q covers learner and logging randomness for fixed ℓ . Both bounds use this same model and cost. Theorem 14 (Paid sparse-feedback benchmark). Suppose additionally that q3T≤mBlogB.q^3T≤ mB B. (28) Then 1128minT,mBTq−m2≤ℛbin∗≤minT, 8mBlogBTq+5m. 1128 \! \T, mBTq \- m2 ^*_ bin≤ \! \T,\,8 mB B\,Tq+5m \. (29) The libraries grow strictly in every phase, total registration cost is B, and every intermediate registration prefix is hard-feasible. 4.2 Proof outline and sublinear regimes The lower construction hides a good identity per phase. The upper learner counts actual switches. Appendix F proves matching up to logarithmic and boundary terms in this restricted regime. Corollary 15 (Learnable sparse-feedback families). For benchmark instances satisfying equation 28, if mBlogBqT⟶0,mT⟶0, mB BqT 0, mT 0, (30) then max0,ℛbin∗/T→0 \0,R^*_ bin/T\→ 0. These conditions force q→0q→ 0 and require effective observations qTqT to dominate identification complexity. The benchmark and published all-q switching bounds (Dekel et al., 2014) have distinct scopes, detailed in Appendix F. 5 Lean formalization Our formal contribution is a compositional verification of native reflection, from probabilistic execution and local contracts to counterfactual regret and sublinear limits. Table 1 identifies its verified connections. Why composition requires verification. Valid component bounds yield a guarantee for the same agent only with compatible trajectory laws, scoring clocks and resource conventions. Our proofs verify marginal preservation, completed-task alignment and adaptive observation moments, establishing that the combined bound concerns the specified native execution. Table 1: Proof obligations addressed by the Lean formalization. Proof obligation Purpose of formal checking Formal result Probability coherence Preserve native laws across couplings. Prop. 4, Thm. 7 Adaptive observations Derive moments under bounded stopping. Lem. 5, Thm. 6 Generation reliability Couple quality, trials and hard costs. Thm. 11, Cor. 13 Deployment stability Control error propagation on actual paths. Thms. 9–10 Composition and limits Align task clocks and limit hypotheses. Thm. 11, Cor. 8 Benchmark consistency Match cost and feedback conventions. Thm. 14 Concrete instantiation Derive interfaces from native execution. Cor. 12, Prop. 16 Reusable guarantees and scope. Concrete native instances derive compatible contracts from generation, validation and execution. Explicit interfaces identify which obligations must be re-established when mechanisms change, supporting reuse of the theory. All thirteen results have Lean proofs (de Moura and Ullrich, 2021; The mathlib Community, 2020) of the end-to-end conditional mathematical implications. Applications must establish their contracts. Appendix H supplies declaration mappings and build provenance for independent checking. 6 Conclusion We connect local generation reliability and deployment stability to conditional native-agent regret, providing a unified view of how reflective mechanisms can affect long-term performance under explicit resource constraints. Concrete native instances demonstrate sublinear regret under hard budgets, repeated growth and imperfect validation. Lean verifies the composed proof chains, complemented by near-matching paid-growth bounds. The resulting framework separates algorithmic guarantees from application-specific assumptions through explicit interfaces, making clear which contracts must be established when generation, validation, or execution mechanisms change. This perspective enables reflective agents to be analyzed through modular guarantees, where improvements in individual components can be incorporated without changing the overall comparison framework. The results establish a foundation for reasoning about adaptive agents whose capabilities evolve through generation, validation, and execution. References Alon et al. (2015) N. Alon, N. Cesa-Bianchi, O. Dekel, and T. Koren Online learning with feedback graphs: beyond bandits. In Proceedings of the 28th Conference on Learning Theory, Vol. 40, p. 23–35. External Links: Link Cited by: Appendix M. Anava et al. (2015) O. Anava, E. Hazan, and S. Mannor Online learning for adversaries with memory: price of past mistakes. In Advances in Neural Information Processing Systems, Vol. 28. External Links: Link Cited by: Appendix M, §2.1. Arora et al. (2012) R. Arora, O. Dekel, and A. Tewari Online bandit learning against an adaptive adversary: from regret to policy regret. In Proceedings of the 29th International Conference on Machine Learning, External Links: Link Cited by: Appendix M, §1, §1, §2.1. Auer et al. (2002) P. Auer, N. Cesa-Bianchi, Y. Freund, and R. E. Schapire The nonstochastic multiarmed bandit problem. SIAM Journal on Computing 32 (1), p. 48–77. External Links: Link Cited by: §2.3. Bubeck and Cesa-Bianchi (2012) S. Bubeck and N. Cesa-Bianchi Regret analysis of stochastic and nonstochastic multi-armed bandit problems. Foundations and Trends in Machine Learning 5 (1), p. 1–122. External Links: Link Cited by: Appendix M, §F.1. Cesa-Bianchi et al. (2013) N. Cesa-Bianchi, O. Dekel, and O. Shamir Online learning with switching costs and other adaptive adversaries. In Advances in Neural Information Processing Systems, Vol. 26. External Links: Link Cited by: Appendix M. Cesa-Bianchi and Lugosi (2006) N. Cesa-Bianchi and G. Lugosi Prediction, learning, and games. Cambridge University Press. External Links: Link Cited by: §2.3. Cheng et al. (2023) D. Cheng, X. Zhou, and B. Ji Understanding the role of feedback in online learning with switching costs. In Proceedings of the 40th International Conference on Machine Learning, p. 5521–5543. External Links: Link Cited by: Appendix M. Daniely et al. (2015) A. Daniely, A. Gonen, and S. Shalev-Shwartz Strongly adaptive online learning. In Proceedings of the 32nd International Conference on Machine Learning, Vol. 37, p. 1405–1411. External Links: Link Cited by: Appendix M. de Moura and Ullrich (2021) L. de Moura and S. Ullrich The Lean 4 theorem prover and programming language. In Automated Deduction—CADE 28, p. 625–635. External Links: Link Cited by: §5. Dekel et al. (2014) O. Dekel, J. Ding, T. Koren, and Y. Peres Bandits with switching costs: T2/3T^2/3 regret. In Proceedings of the 46th Annual ACM Symposium on Theory of Computing, p. 459–467. External Links: Document, Link Cited by: Appendix M, Appendix F, §4.2. Dudík et al. (2011) M. Dudík, J. Langford, and L. Li Doubly robust policy evaluation and learning. In Proceedings of the 28th International Conference on Machine Learning, External Links: Link Cited by: Appendix M. Ghalme et al. (2020) G. Ghalme, S. Dhamal, S. Jain, S. Gujar, and Y. Narahari Ballooning multi-armed bandits. arXiv preprint arXiv:2001.10055. External Links: Link Cited by: Appendix M. Herbster and Warmuth (1998) M. Herbster and M. K. Warmuth Tracking the best expert. Machine Learning 32 (2), p. 151–178. External Links: Link Cited by: §2.3. Lattimore and Szepesvári (2020) T. Lattimore and C. Szepesvári Bandit algorithms. Cambridge University Press. External Links: Link Cited by: Appendix K, Appendix M, §F.1. Madaan et al. (2023) A. Madaan, N. Tandon, P. Gupta, S. Hallinan, L. Gao, S. Wiegreffe, U. Alon, N. Dziri, S. Prabhumoye, Y. Yang, S. Gupta, B. P. Majumder, K. Hermann, S. Welleck, A. Yazdanbakhsh, and P. Clark Self-refine: iterative refinement with self-feedback. In Advances in Neural Information Processing Systems, Vol. 36. External Links: Link Cited by: §1. Merten et al. (2018) S. Merten, A. Bagnall, and G. Stewart Verified learning without regret: from algorithmic game theory to distributed systems with mechanized complexity guarantees. In Programming Languages and Systems (ESOP 2018), Lecture Notes in Computer Science, Vol. 10801, p. 561–588. External Links: Document, Link Cited by: Appendix M, §1. Mourtada and Maillard (2017) J. Mourtada and O. Maillard Efficient tracking of a growing number of experts. In Proceedings of the 28th International Conference on Algorithmic Learning Theory, Vol. 76, p. 517–539. External Links: Link Cited by: Appendix K, Appendix M, §H.1, §1. Nguyen and Mehta (2024) Q. M. Nguyen and N. Mehta Near-optimal per-action regret bounds for sleeping bandits. In Proceedings of the 27th International Conference on Artificial Intelligence and Statistics, Vol. 238, p. 2827–2835. External Links: Link Cited by: Appendix M, §H.1. Nguyen-Tang and Arora (2025) T. Nguyen-Tang and R. Arora Policy-regret minimization in markov games with function approximation. In Proceedings of the 42nd International Conference on Machine Learning, Vol. 267, p. 46242–46264. External Links: Link Cited by: Appendix M, §1. Park et al. (2025) C. Park, X. Liu, A. Ozdaglar, and K. Zhang Do LLM agents have regret? a case study in online learning and games. In International Conference on Learning Representations, External Links: Link Cited by: Appendix M. Rouyer et al. (2021) C. Rouyer, Y. Seldin, and N. Cesa-Bianchi An algorithm for stochastic and adversarial bandits with switching costs. In Proceedings of the 38th International Conference on Machine Learning, Vol. 139, p. 9127–9135. External Links: Link Cited by: Appendix M. Saha et al. (2020) A. Saha, P. Gaillard, and M. Valko Improved sleeping bandits with stochastic action sets and adversarial rewards. In Proceedings of the 37th International Conference on Machine Learning, Vol. 119, p. 8357–8366. External Links: Link Cited by: Appendix M. Shinn et al. (2023) N. Shinn, F. Cassano, A. Gopinath, K. Narasimhan, and S. Yao Reflexion: language agents with verbal reinforcement learning. In Advances in Neural Information Processing Systems, Vol. 36. External Links: Link Cited by: §1. The mathlib Community (2020) The mathlib Community The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, External Links: Document, Link Cited by: §5. Xu et al. (2026) J. Xu, V. Jain, B. Wilder, and A. Singh Online decision making with generative action sets. In International Conference on Learning Representations, External Links: Link Cited by: Appendix M, §H.1, §1. Appendix Appendix A Own-history executions and their realizations A.1 Probability objects and proof of Proposition 4 Write ℋttaskH_t task for the type of completed prefixes and QtA(h,⋅)Q_t^A(h,·) for the next-record kernel of A. Starting from its prescribed initial law ℙA(0)P_A^(0), define the prefix law recursively by kernel integration. For a nonnegative measurable test function f this means ∫f(h,x)dℙA(t+1)(h,x)=∫ℋttask[∫f(h,x)QtA(h,x)]dℙA(t)(h). f(h,x)\,dP_A^(t+1)(h,x)= _H_t task [ f(h,x)Q_t^A(h,dx) ]dP_A^(t)(h). (31) Taking f=1f=1 and using QtA(h,t+1)=1Q_t^A(h,Z_t+1)=1 proves inductively that every prefix law is a probability measure. For a finite event model the inner integrals are ordinary finite sums. For the native measurable model they are the kernel integrals used in NativeSemantics. The comparator construction replaces QAQ^A by QμQ^μ everywhere, including its history argument. Measurability and integrability. Let ℋttaskH_t task denote the finite prefix of the product record space. A normalized measurable control kernel from ℋttaskH_t task to t+1Z_t+1 recursively induces a trajectory probability law. In the companion, this is the causal trajectory construction used by NativeSemantics.Execution.law, not an unrelated measure supplied after the fact. Each score is a measurable function of a completed prefix. Composing with the measurable prefix projection makes YtY_t measurable. Finite summation makes LTL_T measurable. Summing the unit bounds gives 0≤LT≤T0≤ L_T≤ T. Since the trajectory law is a probability measure, the constant T is integrable. Domination proves integrability of LTL_T. Monotonicity of integration gives 0≤JT≤T0≤ J_T≤ T. For a measurable realization rAr_A, the pushforward identity means that its distribution is the actual causal law. Integration under a measurable pushforward gives ∫LTA(rA(ω))Γ(ω)=∫LTA(x)d((rA)#Γ)(x)=∫LTA(x)dℙA(x). L_T^A(r_A(ω))\,d (ω)= L_T^A(x)\,d((r_A)_\# )(x)= L_T^A(x)\,dP_A(x). (32) The preceding integrability argument justifies these real-valued integrals. The formal result is NativeSemantics.Realization.expected_total. Finite loss bounds. For each trajectory x, the unit-score contract gives 0≤∑t=0T−1Yt(x)≤∑t=0T−11=T.0≤ _t=0^T-1Y_t(x)≤ _t=0^T-11=T. (33) Each summand is measurable, hence the finite sum is measurable. The integrable dominating constant has integral T because the law has total mass one. In particular, the comparator loss set is nonempty and bounded below by zero. Its real infimum is therefore the intended mathematical infimum, rather than a default value for an empty or unbounded set. Why the comparator is outside the expectation. Fix a causal procedure μ before evaluating its expectation. Its initial conditions and kernels determine its own law ℙμP_μ. A coupling can correlate exogenous randomness across executions for a proof, but must preserve both marginals. It cannot give μ the library generated by A unless that library would also be generated in the comparator execution. In particular, an infimum over realized paths chosen after all random outcomes is not the infimum in equation 1. Resource modes. The main theorem uses the hard class directly. If a mean class is considered, integrability of prefix costs is an additional prerequisite for ordinary real expectations. The checked inclusion theorem integrates each hard prefix inequality under the own law of the candidate. The hard-class optimum can exceed the mean-class optimum, so changing the comparator class requires changing the objective. It is not a modification of the implementation charge. These ancillary definitions and identities are in ResourceClasses. The revised main theorem does not assume the hard and mean classes coincide. Appendix B Observation and stopping proofs B.1 Local moments in Lemma 5 For this proof only, suppress the slot and history indices. Let I,OI,O be finite types, p(i)>0p(i)>0 with ∑ip(i)=1 _ip(i)=1, and k(i,o)≥0k(i,o)≥ 0 with ∑ok(i,o)=1 _ok(i,o)=1. Let M(i,o)∈0,1M(i,o)∈\0,1\ and y(i,o)∈[0,d]y(i,o)∈[0,d]. Define ℓ^j,o(i)=j=iM(j,o)y(j,o)p(i)q(i),ℙ(J=j,O=o∣h)=p(j)k(j,o). _j,o(i)= 1\j=i\M(j,o)y(j,o)p(i)q(i), (J=j,O=o h)=p(j)k(j,o). (34) All expectations in this subsection refer to this conditional joint law. In particular, the symbols in the estimator are evaluated at the observed event (j,o)(j,o), whereas its coordinate is i. First moment. Fix a completed history and suppress its index. The joint event probability of draw j and outcome o is p(j)k(j,o)p(j)k(j,o). Its sum is one. At coordinate i, all summands with j≠ij≠ i are zero. Hence ∑j,op(j)k(j,o)ℓ^j,o(i)=p(i)p(i)q(i)∑ok(i,o)M(i,o)y(i,o)=ℓref(i). _j,op(j)k(j,o) _j,o(i)= p(i)p(i)q(i) _ok(i,o)M(i,o)y(i,o)= ^ref(i). (35) The division is legitimate because p(i),q(i)>0p(i),q(i)>0. There is no hidden claim that a missing observation is itself a zero task loss. It contributes zero to the estimator and is corrected by the denominator. Second moment. The accepted score satisfies (My)2≤Md2(My)^2≤ Md^2, because M∈0,1M∈\0,1\ and 0≤y≤d0≤ y≤ d. Consequently J,O|hℓ^(i)2≤p(i)q(i)d2p(i)2q(i)2=d2p(i)q(i).E_J,O h (i)^2≤ p(i)q(i)d^2p(i)^2q(i)^2= d^2p(i)q(i). (36) Multiplying by p(i)p(i) and summing proves the second inequality in equation 7. Finite sums also give equality between the expected estimated learner–comparator difference and its true loss difference. The comparator coordinate must be fixed at this history. A coordinate selected using the current draw need not satisfy the same equality. The learner–comparator moment identity. Let v be determined by the completed history, before (J,O)(J,O) is drawn. Finite linearity and equation 35 give J,O|h[∑ip(i)ℓ^J,O(i)−ℓ^J,O(v)] _J,O h\! [ _ip(i) _J,O(i)- _J,O(v) ] =∑ip(i)ℓref(i)−ℓref(v), = _ip(i) ^ref(i)- ^ref(v), (37) J,O|h[ℓref(J)−ℓref(v)] _J,O h[ ^ref(J)- ^ref(v)] =∑ip(i)ℓref(i)−ℓref(v). = _ip(i) ^ref(i)- ^ref(v). (38) Subtracting the two equalities yields zero conditional estimation noise. No independence of the whole past and future is used. Predictability of v is essential because it permits applying the coordinate identity at the fixed coordinate v. B.2 The generated stopped law Let ErE_r be the finite event type at slot r. Complete histories are built recursively from Option(Er)Option(E_r). The terminal value none is absorbing. At an active history the next-event kernel is the normalized local observation kernel on some events. At an inactive history it assigns probability one to none. The Boolean activity rule depends only on the completed history. Let ϖr(h) _r(h) be the resulting prefix mass. Its recursion is ϖ0(())=1,ϖr+1(h,x)=ϖr(h)krstop(h,x). _0(())=1, _r+1(h,x)= _r(h)k_r stop(h,x). (39) Summing over x proves normalization by induction. Nonnegativity follows by multiplying nonnegative local masses. These are actual path probabilities, not importance weights. For any cumulative event score FrF_r, expand one step of the expectation, sum over the last event, and use kernel normalization on the old score. This gives ℙstop(r+1)Fr+1=ℙstop(r)Fr+∑hϖr(h)∑xkrstop(h,x)fr(h,x).E_P^(r+1)_ stopF_r+1=E_P^(r)_ stopF_r+ _h _r(h) _xk_r stop(h,x)f_r(h,x). (40) For the estimation noise, the last sum is zero at inactive histories by definition and zero at active histories by equation 35. Induction proves equation 8. For the quadratic score, retain the actual local expectation instead of replacing it by zero, then apply equation 36. Summing the inequalities with nonnegative prefix masses proves equation 9. These final implications are StoppedObservation.Protocol.stopped_unbiased and stopped_second. They invoke the normalized recursive stopped process, rather than assuming a stopped martingale identity. Detailed induction on the stopped prefix. Set F0=0F_0=0 and Fr+1(h,x)=Fr(h)+fr(h,x)F_r+1(h,x)=F_r(h)+f_r(h,x), with fr=0f_r=0 on the terminal event. Expanding the finite product law gives ∑h,xϖr(h)krstop(h,x)Fr+1(h,x) _h,x _r(h)k_r stop(h,x)F_r+1(h,x) =∑hϖr(h)Fr(h)∑xkrstop(h,x)⏟=1 = _h _r(h)F_r(h) _xk_r stop(h,x)_=1 +∑hϖr(h)∑xkrstop(h,x)fr(h,x). + _h _r(h) _xk_r stop(h,x)f_r(h,x). (41) For estimation noise, the second line vanishes at every history. The expectation remains zero at r+1r+1 if it is zero at r, establishing the first stopped identity from the base case. For the quadratic score, it is bounded by ∑hϖr(h)h is activedr(h)2∑i∈ℐrqr(h,i)−1. _h _r(h)1\h is active\\,d_r(h)^2 _i _rq_r(h,i)^-1. (42) Summing these one-step inequalities for r=0,…,N−1r=0,…,N-1 proves the cumulative capacity bound. Nonnegativity of ϖr _r preserves every inequality. Bounded N makes all sums finite, so no unbounded optional-stopping theorem is being silently applied. Scope of the local modification. The observation kernel must represent the run that is actually being scored. If the chosen identity itself determines how many task rounds are included, inserting its original draw probability into a common-duration estimator is not justified by this proof. The revised statement retains the synchronized accepted-score contract at this precise boundary. The activity rule for the next completed slot remains fully history-adapted. Appendix C Potential and native-transfer proofs C.1 Proof of Theorem 6 Step 1. Positivity and conservation under sharing. The initial total mass is W0=1W_0=1. If Wr>0W_r>0, at least one wr(i)w_r(i) is positive. Since exp(−ηℓ^r(i))>0 (-η _r(i))>0, the tilted mass is positive. Summing the update over j and using ∑jΘr(i,j)=1 _j _r(i,j)=1 proves that sharing preserves this tilted total. Thus Wr+1>0W_r+1>0 by induction and all logarithms and probabilities below are defined. Fix a realized sequence of finite types, transitions, and nonnegative estimates. Let Wr=∑iwr(i)W_r= _iw_r(i). Row stochasticity in equation 3 yields Wr+1=Wr∑ipr(i)e−ηℓ^r(i).W_r+1=W_r _ip_r(i)e^-η _r(i). (43) The exponential is strictly positive. Starting from W0=1W_0=1, every WrW_r is positive. For x≥0x≥ 0, e−x≤1−x+x2/2e^-x≤ 1-x+x^2/2, and logu≤u−1 u≤ u-1 for u>0u>0. Therefore logWr+1−logWr≤−η⟨pr,ℓ^r⟩+η22⟨pr,ℓ^r2⟩. W_r+1- W_r≤-η p_r, _r + η^22 p_r, _r^2 . (44) No upper bound on the importance-weighted estimate is used here. This explains why arbitrarily small positive probabilities are compatible with the expectation proof, though not with an automatic high-probability statement. Step 2. The logarithmic upper bound. For x≥0x≥ 0, e−x≤1−x+x2/2e^-x≤ 1-x+x^2/2. Applying this coordinatewise and summing with probability weights gives Wr+1Wr W_r+1W_r ≤1−η∑ipr(i)ℓ^r(i)+η22∑ipr(i)ℓ^r(i)2, ≤ 1-η _ip_r(i) _r(i)+ η^22 _ip_r(i) _r(i)^2, (45) logWR+1 W_R+1 ≤−η∑r=0R⟨pr,ℓ^r⟩+η22∑r=0R⟨pr,ℓ^r2⟩. ≤-η _r=0^R p_r, _r + η^22 _r=0^R p_r, _r^2 . (46) The first right side is positive because it bounds the strictly positive ratio from above. Applying logu≤u−1 u≤ u-1 to the ratio gives the one-step logarithmic inequality. The second display is its telescoping sum, using logW0=0 W_0=0. Step 3. A supported path lower bound. Define its incoming mass at slot r by ωr=ν0(v0)∏s<rΘs(vs,vs+1)exp(−η∑s<rℓ^s(vs)). _r^v= _0(v_0) _s<r _s(v_s,v_s+1) \! (-η _s<r _s(v_s) ). (47) Induction proves wr(vr)≥ωrw_r(v_r)≥ _r^v. The base case is equality. For the induction step, retain the single nonnegative summand indexed by vrv_r in the update to wr+1(vr+1)w_r+1(v_r+1). Multiplication by the positive transition and exponential preserves the inequality. At the final slot, retain the mass at vRv_R and sum its outgoing row. This is why the final displayed bound uses R transitions but R+1R+1 scored slots. The supported path contributes a nonnegative term to the final total mass. Following it through slots 0,…,R0,…,R gives WR+1≥ν0(v0)∏r<RΘr(vr,vr+1)exp(−η∑r=0Rℓ^r(vr)).W_R+1≥ _0(v_0) _r<R _r(v_r,v_r+1) \! (-η _r=0^R _r(v_r) ). (48) The last update is summed over its destination row, so there is no missing comparator transition after slot R. Taking logs, summing equation 44, and rearranging gives the deterministic path inequality ∑r=0R(⟨pr,ℓ^r⟩−ℓ^r(vr))≤C()η+η2∑r=0R⟨pr,ℓ^r2⟩. _r=0^R ( p_r, _r - _r(v_r) )≤ C(v)η+ η2 _r=0^R p_r, _r^2 . (49) Step 4. Combine the two sides and take expectation. The lower logarithm is −C()−η∑r=0Rℓ^r(vr)-C(v)-η _r=0^R _r(v_r). Comparing it with equation 46, moving the loss terms to one side, and dividing by η>0η>0 proves equation 49. This argument is pointwise for every realized collection of finite types and stochastic transitions. The proof is Growing.growing_path_regret. Integrate on the stipulated comparator coupling. The integrability assumptions permit finite summation and integration to commute. The moment identities identify the left side with actual reference selection differences. The code and quadratic budgets prove equation 12, as in DependentSelection.expected_growing_selection. Compatibility with the observation theorem. To use the local calculation in the expected path theorem, the probabilities prp_r in the event kernels must be those produced by the weight recurrence, and the score difference must be the same random variable. For history-dependent type families, these identifications and integrability are the explicit Experiment contract. The finite stopped-observation result proves moments for its stated event types. It does not construct every possible native observation model. Thus a supplied moment identity is a visible interface premise, not a claimed consequence of unrelated logs. C.2 Proof of Theorem 7 For one fixed comparator, insert every endpoint in its stated order. JAnat−Jμnat= J_A^nat-J_μ^nat= (JAnat−JAref)+(JAref−Jsel)+(Jsel−Jμav)+(Jμav−Jμal) (J_A^nat-J_A^ref)+(J_A^ref-J^sel)+(J^sel-J_μ^av)+(J_μ^av-J_μ^al) (50) +(Jμal−Jμcl)+(Jμcl−Jμpath)+(Jμpath−Jμref)+(Jμref−Jμnat). +(J_μ^al-J_μ^cl)+(J_μ^cl-J_μ^path)+(J_μ^path-J_μ^ref)+(J_μ^ref-J_μ^nat). The selection arrow Jsel−JμavJ^sel-J_μ^av is bounded by Theorem 6. Substitute all seven directed certificates and Vest≤bV_ est≤ bV. This gives equation 14 for a fixed comparator. Proposition 4 identifies the realized native endpoint expectations with their own-law expected losses. The formal result permits comparator-specific coupling measures and type families. Budget substitution without hidden sign assumptions. Substitution into equation 50 first gives JT(A)−JT(μ) J_T(A)-J_T(μ) ≤EA+(F+b+DA)+C/η+ηVest/2+G ≤ E_A+(F+P_b+D_A)+C/η+η V_ est/2+G +bS+hresp(S+1)+DC+Enf+EC. +bS+h_resp(S+1)+D_C+E_ nf+E_C. (51) Since η>0η>0 and Vest≤bV_ est≤ bV, replace only the quadratic term by ηbV/2η bV/2. Substitute b=hresp(⌈T/b⌉+Nb+1)P_b=h_resp( T/b +N_b+1) and group the seven scalar charges into Δ . This produces exactly UTU_T in equation 14. Each adjacent difference is present once. No absolute values or independently maximized versions of individual endpoints are inserted. Write the uniform upper bound as UTU_T. For every μ, the fixed-comparator result states JT(A)−UT≤JT(μ)J_T(A)-U_T≤ J_T(μ). Thus JT(A)−UTJ_T(A)-U_T is a lower bound on the nonempty set of comparator expected losses. The defining greatest-lower-bound property implies JT(A)−UT≤infμJT(μ)J_T(A)-U_T≤ _μJ_T(μ), proving the theorem. There is no exchange of expectation and infimum. Proof of Corollary 8. Divide the definition of UTU_T by its positive horizon. Its normalized value is exactly the sum in equation 15. Finite addition preserves limits, so UT/T→0U_T/T→ 0. The main bound implies 0≤max0,RT/T≤max0,UT/T.0≤ \0,R_T/T\≤ \0,U_T/T\. (52) Continuity of the maximum and squeezing prove convergence. This is checked both as a numerical lemma and as a theorem on families of native executions with interface witnesses. Appendix D Local-feedback stability and resource charging Finite paths and Bellman values. For a kernel sequence K, define Vt,0K(s)=0V^K_t,0(s)=0 and Vt,n+1K(s)=ct(s)+∑jKt(s,j)Vt+1,nK(j).V^K_t,n+1(s)=c_t(s)+ _jK_t(s,j)V^K_t+1,n(j). (53) For an explicit next-state trace, its probability is the product of the traversed kernel probabilities. Inductively summing over the last or first next state proves normalization. Expanding the trace loss and using this normalization proves that the trace expectation equals equation 53. Averaging with the common initial distribution gives JT(K)J_T(K). These equalities are in FeedbackTrajectory, so the Bellman quantity is not merely a proxy with an unproved relation to the objective. Range-sensitive TV inequality. If f(j)∈[a,a+h]f(j)∈[a,a+h] and p,qp,q are probability distributions, their signed mass difference sums to zero. Subtract the midpoint a+h/2a+h/2. Then |∑j(p(j)−q(j))f(j)|=|∑j(p(j)−q(j))(f(j)−a−h/2)|≤h2∑j|p(j)−q(j)|=hTV(p,q). | _j(p(j)-q(j))f(j) |= | _j(p(j)-q(j))(f(j)-a-h/2) |≤ h2 _j|p(j)-q(j)|=hTV(p,q). (54) For zero TV the distributions agree on the finite set, so the expectation difference is zero without imposing a range condition. D.1 Proof of Theorem 9 Step 1. Exact one-step difference. For a remaining horizon n+1n+1, add and subtract the same reference continuation under KtK_t. Vt,n+1K(s)−Vt,n+1L(s) V^K_t,n+1(s)-V^L_t,n+1(s) =∑jKt(s,j)Vt+1,nK(j)−Vt+1,nL(j) = _jK_t(s,j)\V^K_t+1,n(j)-V^L_t+1,n(j)\ +∑jKt(s,j)−Lt(s,j)Vt+1,nL(j). + _j\K_t(s,j)-L_t(s,j)\V^L_t+1,n(j). (55) The common immediate score cancels. Taking absolute values uses the triangle inequality and Kt(s,j)≥0K_t(s,j)≥ 0. The second sum is bounded by the range-sensitive TV inequality. If the local TV is zero, the distributions agree and this term is zero without a range condition. Subtract the two Bellman equations and add and subtract the K-average of the reference continuation. The immediate scores cancel because they are the same function of the complete pre-update state. Writing ζt(s)=ht(s)εt(s) _t(s)=h_t(s) _t(s) gives |Vt,n+1K(s)−Vt,n+1L(s)|≤∑jKt(s,j)|Vt+1,nK(j)−Vt+1,nL(j)|+ζt(s).|V^K_t,n+1(s)-V^L_t,n+1(s)|≤ _jK_t(s,j)|V^K_t+1,n(j)-V^L_t+1,n(j)|+ _t(s). (56) The second term follows from equation 54 and the local contract. Induction on n, starting at zero continuation, bounds the right side by the K-Bellman value of the accumulated charge ζ. Averaging at time zero and using the trace interpretation proves equation 17. Step 2. Propagate local charges along the native law. Define t,0(s)=0D_t,0(s)=0 and t,n+1(s)=ζt(s)+∑jKt(s,j)t+1,n(j).D_t,n+1(s)= _t(s)+ _jK_t(s,j)D_t+1,n(j). (57) At n=0n=0, both value differences are zero. If |Vt+1,nK−Vt+1,nL|≤t+1,n|V^K_t+1,n-V^L_t+1,n| _t+1,n, nonnegativity of KtK_t and equation 56 imply the same bound at (t,n+1)(t,n+1). Therefore |V0,TK−V0,TL|≤0,T|V^K_0,T-V^L_0,T| _0,T. Averaging over the common initial distribution pinitp init yields |JT(K)−JT(L)| |J_T(K)-J_T(L)| ≤∑spinit(s)|V0,TK(s)−V0,TL(s)| ≤ _sp init(s)|V^K_0,T(s)-V^L_0,T(s)| ≤∑spinit(s)0,T(s)=ℙK∑t<Tζt(St). ≤ _sp init(s)D_0,T(s)=E_P_K _t<T _t(S_t). (58) The final equality is the finite trajectory/Bellman identity, applied to the nonnegative score ζ instead of the task score c. It fixes the law as ℙKP_K, not a worst-case union of possible update times. Step 3. The hard-resource inequality. For the hard-resource version, the pointwise hypotheses yield 0≤ζt(s)≤H¯ε¯χt(s)≤H¯ε¯cminrt(s).0≤ _t(s)≤ H _t(s)≤ H c_ r_t(s). (59) Monotonicity of the K-Bellman recursion transfers this inequality to path expectations. For every positive-mass trace the cumulative resource is at most BTB_T. Zero-mass traces contribute zero, irrespective of their values. Normalization therefore gives ℙK∑trt(St)≤BTE_P_K _tr_t(S_t)≤ B_T. Substitute in equation 17 to prove equation 18. No worst-case union over possibly active times is introduced. For the local-only alternative, induction in equation 53 gives 0≤Vt,nL≤n0≤ V^L_t,n≤ n. At boundary t, the remaining continuation has at most T−t−1T-t-1 scores. Hence |JT(K)−JT(L)|≤∑t<T(T−t−1)ε¯T≤T2ε¯T.|J_T(K)-J_T(L)|≤ _t<T(T-t-1) _T≤ T^2 _T. (60) This argument does not assume mixing or forgetting. Its precision condition is correspondingly stronger. Proof of Theorem 10. For each fixed comparator, insert the two reference expectations. JT(KA)−JT(Kμ)=[JT(KA)−JT(LA)]+[JT(LA)−JT(Lμ)]+[JT(Lμ)−JT(Kμ)].J_T(K_A)-J_T(K_μ)=[J_T(K_A)-J_T(L_A)]+[J_T(L_A)-J_T(L_μ)]+[J_T(L_μ)-J_T(K_μ)]. (61) Bound the first and last terms by equation 18, and invoke the proved reference transfer for the middle term. Uniformity in μ permits the same infimum argument used for Theorem 7. In Lean, NativeRepairEndpoint.counterfactual calls ModelMain.main_fixed, together with actual kernel-path bounds. It does not accept the desired reference regret conclusion as a new axiom. Its resource-side structure contains local TV and influence bounds, local cost domination, and a hard path budget. For no regret, normalize equation 19. The sum of UT/TU_T/T, a fixed constant times BA/TB_A/T, and a fixed constant times BC/TB_C/T tends to zero. Apply equation 52. For equation 60, division by T gives Tε¯T _T, whose assumed convergence proves the alternative. Appendix E Local generation and the combined native theorem Finite causal trial laws. Fix episode e and suppress e on its trial quantities. Let ℋe,kgenH_e,k gen be the finite type of completed trial outcomes in an episode. A normalized nonnegative kernel gk(h,i)g_k(h,i) selects the next outcome. Write ℙe(k)P_e^(k) for the completed-trial law, with mass ϖkgen(h) _k gen(h). Its mass recursion satisfies ϖ0gen(())=1 _0 gen(())=1 and ϖk+1gen(h,i)=ϖkgen(h)gk(h,i) _k+1 gen(h,i)= _k gen(h)g_k(h,i). The outcome can encode a candidate, validation, and retention. A success indicator bk(h,i)∈0,1b_k(h,i)∈\0,1\ marks an outcome whose retained card supports the stipulated causal available path. It may depend on the comparator fixed for the proof and on completed history, but is not an oracle supplied to the generator. Let ξ0=1 _0=1 and ξk+1(h,i)=ξk(h)(1−bk(h,i)) _k+1(h,i)= _k(h)(1-b_k(h,i)). On still-unsuccessful histories assume ∑igk(h,i)(1−bk(h,i))≤1−ρ,0<ρ≤1. _ig_k(h,i)(1-b_k(h,i))≤ 1-ρ, 0<ρ≤ 1. (62) Expand one step of the actual law. ℙe(ξk+1=1) _e( _k+1=1) =∑hϖkgen(h)ξk(h)∑igk(h,i)(1−bk(h,i)) = _h _k gen(h) _k(h) _ig_k(h,i)(1-b_k(h,i)) (63) ≤(1−ρ)∑hϖkgen(h)ξk(h)=(1−ρ)ℙe(ξk=1). ≤(1-ρ) _h _k gen(h) _k(h)=(1-ρ)P_e( _k=1). (64) Successful-history terms vanish. All remaining path masses are nonnegative. Induction from probability one gives ℙe(ξk=1)≤(1−ρ)kP_e( _k=1)≤(1-ρ)^k, without trial independence. The checked result is LocalGenerationCertificate.failure_bound. Local quality and the semantic endpoint. For completed trial history h, let gtpre(h)g pre_t(h) and gtpost(h)g post_t(h) be conditional expected task differences between a specified causal available path and its aligned ideal path. Their exact finite-law expectation must equal the corresponding part of Jμav−JμalJ_μ^av-J_μ^al. This is a semantic identification, not a bound on the generation opportunity gap. An application must derive it from the score laws and a disjoint episode decomposition. Assume gtpre(h)≤1g pre_t(h)≤ 1 on τ delay tasks and gtpost(h)≤δ+ξk(h)g post_t(h)≤δ+ _k(h) on n later tasks. Then ℙe(k)[∑t<τgtpre+∑t<ngtpost] _P_e^(k) [ _t<τg pre_t+ _t<ng post_t ] ≤ℙe(k)[τ+nδ+nξk] _P_e^(k)[τ+nδ+n _k] (65) ≤τ+n[δ+(1−ρ)k]. ≤τ+n[δ+(1-ρ)^k]. (66) The first inequality sums local bounds with nonnegative masses. Normalization evaluates constants. The second uses the proved failure bound. This is Episode.gap_le, not a field assuming a small total gap. Episodes need not be independent, but their laws must describe their actual contributions. Random entry histories require uniformly valid conditional contracts and the correct marginal or conditional representation. Resetting history in the proof while keeping its effects in the deployment is invalid. Sum equation 66 to obtain equation 20. Nonnegative envelopes and ∑ene≤T _en_e≤ T give AT+T(δT+fT)A_T+T( _T+f_T) by finite summation and monotonicity. Uniform envelopes without separating an infimum. The comparison is first proved for a single fixed μ, with its own episode laws. For each episode, ne≥0n_e≥ 0 and the envelope bounds imply τe+ne[δe+(1−ρe)ke]≤τe+ne(δT+fT). _e+n_e[ _e+(1- _e)^k_e]≤ _e+n_e( _T+f_T). (67) Summing, using ∑eτe≤AT _e _e≤ A_T, ∑ene≤T _en_e≤ T, and δT+fT≥0 _T+f_T≥ 0 gives gTgen(μ)≤AT+(δT+fT)∑ene≤AT+T(δT+fT).g_T gen(μ)≤ A_T+( _T+f_T) _en_e≤ A_T+T( _T+f_T). (68) Uniformity means these same numeric envelopes work for every comparator, although its episode laws may differ. There is no step that independently optimizes one envelope for one comparator and another envelope for a different comparator. The combined endpoint. The formal structure Remainder retains acquisition, alignment, response, representation, and capacity conditions. It has no generation or deployment bound. The constructor Remainder.certify derives generation from episodes, identifies the inner deployment endpoints, and assigns zero to their budgets. The theorem native_local invokes the actual reference theorem with this constructed witness and the two local kernel-resource contracts. Thus the outer native kernel comparison includes any selector discrepancy, not just changes to displayed feedback. The validated CompletedNativeV19.Instance.bound carries the kernels, reference experiment, episodes, integrable score endpoints, and completed-task identities. Its generation budget is defined by delay, quality, and failure envelopes, while its inner reference deployment arrows are identities. Its conclusion is the original own-history regret. No bound on that regret or on either derived total gap is an input. Other reference interfaces remain explicit. Subtracting the generation budget from the reference bound leaves exactly UTrestU_T rest, proving equation 21 without duplicate deployment charges. Exact budget identity. Let UTU_T be the reference upper bound with its generation budget G=AT+T(δT+fT)G=A_T+T( _T+f_T) and internal deployment budgets zero. By definition UTrest=UT−GU_T rest=U_T-G. Consequently RT R_T ≤UT+κBA+κBC ≤ U_T+κ B_A+κ B_C =UTrest+AT+T(δT+fT)+κ(BA+BC). =U_T rest+A_T+T( _T+f_T)+κ(B_A+B_C). (69) The first line is an application of the proved transfer, with the generation certificate just constructed. The second is an exact scalar identity. No adjacent endpoint difference may be charged twice. The same causal mechanism can affect different adjacent differences, which must both be retained. An outer full-state charge already covers propagation of its own perturbation. Appendix L gives an explicit accounting example. The family no-regret theorem. Each horizon supplies a complete instance of the stated model and contracts. Its finite state domains, trial-outcome domains, episode index set, comparator coupling laws, and reference identity domains may vary with the horizon. Uniformity of a budget is over comparators at that horizon, not over all horizons. The formal family uses a common ambient measurable space and comparator index type. These do not require identical kernels or identical finite domains across horizons. Divide equation 21 by T>0T>0. With fixed ρ∈(0,1]ρ∈(0,1] and κ, its normalized upper bound is UTrestT+ATT+δT+(1−ρ)kT+κBA(T)+BC(T)T. U_T restT+ A_TT+ _T+(1-ρ)^k_T+κ B_A(T)+B_C(T)T. (70) Because 0≤1−ρ<10≤ 1-ρ<1 and kT→∞k_T→∞, the geometric term tends to zero. Each remaining term tends to zero under the hypotheses of Theorem 11. This argument uses the combined resource condition directly, without adding separate resource limits. The positive part is continuous, so equation 52 proves the claimed upper no-regret limit. The publication endpoint is CompletedNativeV19.variable_family. For each family index it invokes the validated completed-task bound, then combines the geometric and normalized limits with denominator T, not T+1T+1. It does not take the desired regret bound as a premise. The earlier LocalNativeFamily.no_regret remains a fixed-domain family result with separately normalized resource assumptions. The earlier correspondence endpoint remains a state-score family result. The new wrapper supplies the completed-task, variable-domain and combined-resource correspondence without changing equation 21. Strength and cost of the assumptions. The available path must be causal, not chosen retrospectively from favorable trial outcomes. Retention and comparator-relative quality must persist on the episode being charged. If increasingly precise good cards become rarer, their smaller hazards must be reflected in fTf_T. A fixed positive hazard cannot be presumed for many mutually exclusive targets. Attempts also consume actual generation and validation resources. Increasing their number is legitimate only when delay and hard budgets permit it. These restrict the admissible native model class, not the original architecture. They are not proved properties of every deployed reflector. Appendix F The finite paid lower and upper benchmark The sparse-family conditions force q→0q→ 0, not unlearnability at fixed q. This benchmark does not lower-bound every native certificate. Published all-q switching constructions (Dekel et al., 2014) address a broader regime. F.1 Information lower bound for the full causal class Finite information construction. In a phase with K identities, choose a hidden target uniformly. Its independent binary base losses have mean 1/2−ϵ1/2-ε, while other identities have mean 1/21/2. Let ℙ0P_0 be the all-1/21/2 observation law and ℙjP_j the target-j law for the same causal randomized learner. The erasure symbol is distinct from a zero loss. All laws are constructed from finite kernels on visible histories. The Bernoulli divergence and erasure calculation give, for 0≤ϵ≤1/40≤ε≤ 1/4, DKL(Ber(1/2)∥Ber(1/2−ϵ))=−12log(1−4ϵ2)≤4ϵ2.D_KL(Ber(1/2)\|Ber(1/2-ε))=- 12 (1-4ε^2)≤ 4ε^2. (71) Independent erasure multiplies this divergence by q. On each completed visible history the learner uses the same conditional action kernel under both environments. Its factor cancels in the supported finite chain rule. If NjN_j counts draws of j, induction on history length yields the divergence bound 4qϵ2ℙ0Nj4qε^2E_P_0N_j. Finite testing inequalities then give ℙjNj≤ℙ0Nj+n4qϵ2ℙ0Nj.E_P_jN_j _P_0N_j+n 4qε^2E_P_0N_j. (72) The divergence calculation in detail. For u=4ϵ2∈[0,1/4]u=4ε^2∈[0,1/4], the elementary inequality −log(1−u)≤u/(1−u)- (1-u)≤ u/(1-u) implies −12log(1−4ϵ2)≤2ϵ21−4ϵ2≤83ϵ2≤4ϵ2.- 12 (1-4ε^2)≤ 2ε^21-4ε^2≤ 83ε^2≤ 4ε^2. (73) Let Eq(p)E_q(p) be the distribution on ⊥,0,1\ ,0,1\ assigning mass 1−q1-q to erasure and mass qp(b)qp(b) to bit b. The erasure contribution to relative entropy is zero and the factors q cancel in each non-erased likelihood ratio. Thus DKL(Eq(p)∥Eq(p′))=∑b∈0,1qp(b)logqp(b)qp′(b)=qDKL(p∥p′).D_KL(E_q(p)\|E_q(p ))= _b∈\0,1\qp(b) qp(b)qp (b)=qD_KL(p\|p ). (74) At q=1q=1 the zero-mass erasure term is omitted. Positive Bernoulli probabilities on both sides ensure the same observation support. At a fixed visible history h, write ptlow(i∣h)p_t low(i h) for the learner action kernel. This same function is used under ℙ0P_0 and ℙjP_j, even though the distributions of h differ. On an action with positive mass, its factor cancels in the likelihood ratio. The next-event divergence is consequently ptlow(j∣h)qDKL(Ber(1/2)∥Ber(1/2−ϵ)).p_t low(j h)\,q\,D_KL(Ber(1/2)\|Ber(1/2-ε)). (75) For all other actions the observation laws agree. Induction with the supported finite chain rule adds these conditional divergences under the null prefix law. Since Nj=∑t<nIt=jN_j= _t<n1\I_t=j\, DKL(ℙ0∥ℙj) D_KL(P_0\|P_j) ≤4qϵ2∑t<nℙ0(t)ptlow(j∣Ht) ≤ 4qε^2 _t<nE_P_0^(t)p_t low(j H_t) =4qϵ2ℙ0Nj. =4qε^2E_P_0N_j. (76) Finally Nj∈[0,n]N_j∈[0,n], so its expectation difference is at most nTV(ℙ0,ℙj)nTV(P_0,P_j). The included finite testing inequality bounds this TV by DKL(ℙ0∥ℙj) D_KL(P_0\|P_j), a conservative constant form. Combining with equation 76 proves equation 72. The proof handles zero-probability action histories on their support. It does not require the learner to assign positive probability to every action. Write xj=ℙ0Njx_j=E_P_0N_j, yj=ℙjNjy_j=E_P_jN_j. Since exactly one identity is selected per primitive round, ∑jxj=n _jx_j=n. Cauchy–Schwarz bounds the sum of square roots in equation 72. Set ϵ=min1/4,K/(64qn).ε= \1/4, K/(64qn)\. (77) Then 64qϵ2n≤K64qε^2n≤ K, and the calculation gives K−1∑jyj≤3n/4K^-1 _jy_j≤ 3n/4. Expected regret against the hidden target is at least ϵn/4ε n/4, which is at least minn,Kn/q/32 \n, Kn/q\/32. The scalar rate, the counts, and the underlying path distributions are all part of the proof chain, rather than a supplied information lower-bound certificate. The count calculation and constants. Because ∑jxj=n _jx_j=n, Cauchy–Schwarz gives ∑jxj≤Kn _j x_j≤ Kn. Averaging equation 72 therefore gives 1K∑jyj≤nK+n4qϵ2n/K≤n2+n4=3n4. 1K _jy_j≤ nK+n 4qε^2n/K≤ n2+ n4= 3n4. (78) The second inequality uses K≥2K≥ 2 and 64qϵ2n≤K64qε^2n≤ K. Against hidden target j, expected base regret is ϵ(n−yj)ε(n-y_j), because each non-target draw loses ϵε in conditional mean. Its average is at least ϵn/4ε n/4. Substitution of equation 77 gives ϵn/4=minn/16,Kn/q/32≥132minn,Kn/q.ε n/4= \n/16, Kn/q/32\≥ 132 \n, Kn/q\. (79) The finite KL/testing lemmas used before this calculation belong to the included proof closure. Classical references describe the general information method (Lattimore and Szepesvári, 2020; Bubeck and Cesa-Bianchi, 2012), but no numerical lower bound from those references is inserted as an axiom. Random tables and fixed instances. The loss table can be sampled before play. A finite factorization expresses the joint expectation as an expectation over complete oblivious tables followed by the learner and logging expectation conditional on each table. An average at least L implies at least one fixed table has conditional expected regret at least L. Independent phase targets allow the argument to be conditioned on every preceding visible phase transcript. Thus it applies to the full causal phase-controller class, not just to independently restarted learners. For the paid schedule, each eligible set has size between B/2B/2 and B. Adding phases, applying the half-scale task definition equation 26, and charging comparator boundary switches produces the left side of equation 29. The explicit constant 1/1281/128 is conservative. The proof uses the actual growing identity types in both the learner and the comparator, as recorded in PaidInformationLower.paid_minimax_lower. F.2 The primitive upper algorithm and its tuning Public construction. Within phase j, the public learner uses uniform initialization and a held-run cap and learning rate determined by Kj,n,qK_j,n,q. Primitive execution records the identity emitted on every round. The proof identifies this primitive algorithm with its exponential-weights state recursion and counts the switches in the emitted identities. A partial final run is treated explicitly. No equality between a macro-policy and an unrelated primitive process is postulated. For roundwise independent masks MtM_t, the run estimator for a fixed eligible identity is Jr=ipr(i)−1∑t∈rMtℓtbase(i)/q1\J_r=i\p_r(i)^-1 _t _rM_t base_t(i)/q. Expanding its square separates the diagonal terms from the cross-time terms. Independence gives a diagonal bound proportional to ur/qu_r/q and a cross-time bound proportional to ur2u_r^2. Applying exponential weights and charging actual held-run switches gives the phase bound. Phase composition, the actual boundary costs, and uniform library bounds give equation 86. These steps terminate at PrimitiveJointBounds.uniform_minimax_upper, in the same primitive minimax model as the lower bound. Runwise variance, including cross-time terms. Here rT_r is the consecutive task-index set in run r, ur=|r|u_r=|T_r|, and u denotes one such length. In the following local calculation s=1,…,us=1,…,u numbers positions inside the run, not internal operations. The vector =(M1,…,Mu)M=(M_1,…,M_u) contains its independent observation masks. The law ℙA,ℓ,qphaseP phase_A, ,q below is the induced phase law of the specified upper learner, with the loss table fixed. The symbols LphasetaskL task_ phase and Lphasebase(i)L base_ phase(i) denote its cumulative task loss and the cumulative base loss of fixed identity i in that phase. Fix the oblivious table and the history at the start of a held run of length u. Conditional on J=iJ=i, let Xi=∑s=1uMsℓsbase(i)/qX_i= _s=1^uM_s base_s(i)/q. Independent Bernoulli masks give |J=i,h[Xi2] _M J=i,h[X_i^2] =1q∑sℓsbase(i)2+2∑s<tℓsbase(i)ℓtbase(i) = 1q _s base_s(i)^2+2 _s<t base_s(i) base_t(i) ≤u/q+u(u−1)≤u/q+u2. ≤ u/q+u(u-1)≤ u/q+u^2. (80) For ℓ^(i)=J=iXi/p(i) (i)=1\J=i\X_i/p(i), it follows that J,M|h∑ip(i)ℓ^(i)2≤K(u/q+u2).E_J,M h _ip(i) (i)^2≤ K(u/q+u^2). (81) For run lengths bounded by b and totaling n, ∑u2≤bnΣ u^2≤ bn and ∑u=nΣ u=n. Thus the phase capacity is Vphase=Kn(b+1/q)V_ phase=Kn(b+1/q). In particular, the whole squared run loss is not multiplied by 1/q1/q. Such a replacement would conflate one observation per run with independent per-round erasure. Exact public tuning. Write a=KlogKa=K K and set b=minn,max1,⌈(n/a)1/3⌉,Vphase=Kn(b+1/q),η=2logK/Vphase.b= \n, \1, (n/a)^1/3 \\, V_ phase=Kn(b+1/q), η= 2 K/V_ phase. (82) These are the TunedPhase parameters. They depend on public n,K,qn,K,q, not on the optimal arm or future losses. Since n≥1n≥ 1, K≥2K≥ 2, and q>0q>0, both b and η are positive. Holding an identity creates no within-run switch. Counting boundaries and the possible incomplete last run bounds internal switching by n/b+1n/b+1. The checked primitive-to-run correspondence then yields ℙA,ℓ,qphase[Lphasetask]−12Lphasebase(i) _P phase_A, ,q[L task_ phase]- 12L base_ phase(i) ≤12logK/η+ηVphase/2+n/b+1 ≤ 12\ K/η+η V_ phase/2+n/b+1\ =122logKVphase+n/b+1. = 12\ 2 K\,V_ phase+n/b+1\. (83) The equality follows from η2Vphase=2logKη^2V_ phase=2 K. Dividing by 2η>02η>0 gives logK/η=ηVphase/2 K/η=η V_ phase/2, and both terms sum to ηVphase=2logKVphaseη V_ phase= 2 K\,V_ phase. Integer caps and short phases. The formal tuning proof treats the cap cases separately. If a≥na≥ n, the capped run size is 11 and the phase task loss bound n is already at most a1/3n2/3a^1/3n^2/3. If a<na<n, put x=(n/a)1/3>1x=(n/a)^1/3>1. Here a≥1a≥ 1 and n≥1n≥ 1 imply x≤nx≤ n, so x≤b≤x+1≤2x≤ b≤ x+1≤ 2x. Consequently 2anb≤2a1/3n2/3,n/b≤a1/3n2/3. 2anb≤ 2a^1/3n^2/3, n/b≤ a^1/3n^2/3. (84) Also 2logKVphase≤2anb+2an/q 2 K\,V_ phase≤ 2anb+ 2an/q. Combining these estimates, or using the trivial bound in the short-phase case, gives the conservative phase bound 4a1/3n2/3+an/q+14\a^1/3n^2/3+ an/q+1\. The checked implementation includes its final partial run and actual emitted identities. Phase composition and a single controller class. One additional boundary switch costs at most 1/21/2 per phase. The upper controller resets its weights at the public phase boundaries, while the lower bound allows every causal controller to retain past history. Both controllers are nevertheless members of the same class A. Since Kj≤BK_j≤ B and xlogx x is increasing for x≥1x≥ 1, summing the phase bounds and using T=mnT=mn gives m(BlogB)1/3n2/3=(mBlogB)1/3T2/3,mBlogBn/q=mBlogBT/q.m(B B)^1/3n^2/3=(mB B)^1/3T^2/3, m B B\,n/q= mB B\,T/q. (85) The additive 4m+m/24m+m/2 is bounded by 5m5m. Taking the supremum over fixed tables and then the infimum over controllers preserves this upper bound because the displayed public controller is admissible. The preceding primitive argument gives the explicit bound ℛbin∗≤4((mBlogB)1/3T2/3+mBlogBT/q)+5m.R^*_ bin≤ 4 ((mB B)^1/3T^2/3+ mB B\,T/q )+5m. (86) Proof of the sparse simplification. Let x=a1/3T2/3x=a^1/3T^2/3 and y=aT/qy= aT/q, with a,T,q>0a,T,q>0. Then x3=aT2x^3=aT^2 and y2=aT/qy^2=aT/q. Multiplying q3T≤aq^3T≤ a by the nonnegative factor a2T3a^2T^3 shows x6≤y6x^6≤ y^6. Both x and y are nonnegative, so monotonicity of the sixth power implies x≤yx≤ y. Substitute into equation 86. Independently, cumulative task loss is at most T and the comparator task loss is nonnegative. The minimax value is therefore at most T. These two upper bounds prove the minimum in equation 29. The registration assertions are not inferred from the loss bound. They are separate arithmetic theorems about equation 25. Every phase creates at least one identity under B≥4mB≥ 4m, the increments telescope to the total budget, and each intermediate registration prefix is bounded by the phase endpoint. Their conjunction with the minimax statements is checked in PrimitiveJointBounds.paid_common_model. Proof of Corollary 15. For positive T,qT,q and nonnegative a, aT/qT=aqT. aT/qT= aqT. (87) This follows by squaring both nonnegative sides, or by the square-root scaling identity. Take a=mBlogBa=mB B. Continuity of the square root and equation 30 show that the normalized upper bound tends to zero. Apply equation 52. The proof in SparseFeedbackBenchmark.sparse_no_regret includes the normalization identity rather than treating asymptotic notation as an informal replacement for it. Appendix G How to instantiate the native transfer This section describes obligations for general applications. Appendix I separately discharges them for a specified verified-template reflector. Neither section reports measurements of a deployed language model. Consider a frozen-weight coding agent whose completed record contains the task, generated program, test report, memory, versioned rule cards, and remaining validation budget. A fixed scorer maps the structured test report to a value in [0,1][0,1]. A rule card induces the execution policy πi _i. The native controller μA _A is retained, rather than replaced by Algorithm 1. State and identity. The state must retain all components needed to predict future task scores. A card identifier names an immutable program and interpreter version, not its current probability of selection. If a finite-state local theorem is used, a finite alphabet and bounded storage must be specified, including the environment state needed for the Markov representation. Bounded prompt length alone does not make an unbounded external environment finite-state. An abstraction that discards state requires its own justified comparison, not an assertion that the finite theorem applies unchanged. Reference observation interface. An evaluator must identify a synchronized score unit, the draw probability pr(i)p_r(i), and the acceptance probability qr(i)q_r(i). Randomly accepting complete test reports independently of their score is one way to meet the accepted-score identity. An evaluator that retains only successful tests is not. A rule card generated after an outcome is available for the next draw, not for the draw that generated that outcome. Endogenous termination of future slots is allowed, whereas changing the current score window after seeing a favorable outcome requires a separate analysis. Local feedback interface. Specify a native raw-feedback kernel KtK_t and a processed-feedback reference kernel LtL_t on the same complete state space. The required quantity is their total variation, including the joint distribution of generated cards, memory, resources, and runtime outcomes. Preserving the mean of the displayed score does not imply this condition. Theorem 9 requires a uniform continuation-value range at perturbed states. Such a range needs a mixing, reset, or bounded-influence argument on the complete state. Deleting a card after a fixed number of rounds does not prove that argument. If no such property is available, only the explicitly weaker local-only bound is supplied here. Resources, generation, and selection are different obligations. Count failed generation and validation attempts whenever their resource is consumed. A strictly positive minimum resource cost controls the number of active updates on each native path. Theorem 11 derives the generation certificate from conditional coverage, per-task quality, and a causal available path. The number of registered cards alone proves none of these conditions. Finally, a native selection bridge must compare complete native and reference executions. An offline reference that receives logs from the native run is not automatically distributed as the online reference used in the potential argument. The learner law must stay fixed across comparator couplings. Proved claims and required application evidence. The moment and potential bounds follow from the actual reference recursion and its stated local observation contract. The stability charge follows from complete-state TV, continuation range, and pathwise costs. The remaining directed certificates are assumptions to establish for the chosen model, preferably from local operational lemmas rather than from measured total regret. Finite observational data alone does not prove a uniform counterfactual certificate over all histories. A statistical validation theorem would need a specified sampling design, coverage assumptions, and uncertainty bounds. No such empirical certificate is claimed in this paper. No duplicate charging. Choose the reference endpoints before evaluating any error. A local-feedback charge can replace the corresponding deployment certificate, or can compare a new outer pair of executions as in Theorem 10. It cannot be added to an unchanged certificate for the same endpoint difference. Different adjacent differences may share a causal source. Resource feasibility restricts the comparator domain. Resource-induced displacement contributes to F only if it displaces a task opportunity not already included in another endpoint. The paid benchmark registers births under its hard budget and charges actual switches in its task loss. Neither cost is an additional generic penalty in the native objective. Appendix H Declaration-level verification map Definitions 1–3 and the thirteen theoretical results use a single numbering sequence. Definitions fix semantic objects and are not themselves proof claims. Table 2 records the checked endpoints. Intermediate declarations are reached through their Lean imports. Corollary 12 constructs a specified native model and derives its interfaces. Proposition 16 adds repeated native growth and derives the persistent cost of false acceptance. Other applications must still establish their own contracts. The release includes a machine-readable mapping with source and build hashes. Table 2: Numbered results and their checked Lean endpoints. Prefix DRGPR. is omitted. Result Formal endpoint Proposition 4 NativeSemantics.Execution.expected_bounds, loss_integrable, and Realization.expected_total Lemma 5 FiniteObservation.Round.estimate_mean, weighted_second, and StoppedObservation.Protocol.stopped_unbiased, stopped_second Theorem 6 DependentSelection.expected_growing_selection Theorem 7 NativeFamily.own_coupling_counterfactual Corollary 8 NativeNoRegret.budget_tends_zero and NativeFamily.own_coupling_no_regret Theorem 9 StateFeedbackStability.actual_loss, adaptive_resource_loss, and module FeedbackLocalOnly, declaration uniform_local_bound Theorem 10 NativeRepairEndpoint.counterfactual, no_regret, and FeedbackLocalOnly.local_only_rate Theorem 11 LocalGenerationCertificate.Episode.gap_le, uniform_budget, CompletedNativeV19.Instance.bound, and CompletedNativeV19.variable_family Corollary 12 Module ConcreteReflection, declarations execution_identity, conditional_main, instantiated_bound, family_bound, square_rate, and no_regret Corollary 13 Module JointGenerationBudget, declarations native_joint, hard_prefix, variable_family, and polynomial_allocation Theorem 14 SparseFeedbackBenchmark.paid_sparse_capped and PrimitiveJointBounds.paid_common_model Corollary 15 SparseFeedbackBenchmark.sparse_no_regret Proposition 16 Module ImperfectGrowth, declarations pointer_error, actual_execution, actual_regret, full_transfer, actual_no_regret, and sublinear_resources H.1 Meaning of end-to-end verification The import root includes the correspondence, clock, validated-instance, observation-law and concrete-reflection modules. The publication wrapper scores completed tasks with the proved padding identity and requires integrable intermediate endpoints. Appendix L maps its supporting derivations. Exact declaration counts, source hashes and build provenance are recorded in the release manifest. These support the thirteen numbered paper results. Declaration count is not a measure of scientific novelty. There are three distinct levels. At the declaration level, every numbered result maps to checked Lean declarations under their displayed hypotheses. At the conditional composition level, the combined endpoint invokes proved selection, generation, and native kernel-transfer results before taking the counterfactual infimum, and the family theorem invokes this endpoint before proving convergence. This is the mathematical chain certified by the artifact. At the concrete deployment level, one would additionally need a particular reflector, its scoring and logging implementation, and proofs that they instantiate every input contract. This third claim is not made. In particular, the Experiment structure contains integrability, supported-path, moment, and capacity obligations. The local observation theorem proves moment identities for its specified finite interface. An instantiation must connect that interface to the same recurrence and probability law. Likewise, Remainder retains acquisition, alignment, history-response, representation, and capacity conditions. The new local theorem derives generation and deployment charges, not these remaining conditions. Compilation of an implication does not convert its assumptions into facts about a real model. The companion contains exact source hashes, per-declaration axiom logs, and a dependency-closed source set. Only propext, Classical.choice, and Quot.sound are allowed. There is no sorryAx or custom regret axiom. English statements and their Lean types were compared manually. The Lean kernel and the recorded dependency environment are trusted, rather than verified by this paper. Citations document prior work, not a claim that all cited papers have been formalized. Earlier broader claims are not verified. The previous all-q multiscale switching-rate claim is not a theorem of this version. Neither is a universal equivalence between raw-real native reflection and bit-feedback reflection, nor a universal validity claim for current-draw-dependent run stopping. The local restrictions in the revised statements are substantive and are recorded in the change audit. They are not represented as successful proofs of the broader earlier statements. Position relative to related models. Tracking growing expert pools (Mourtada and Maillard, 2017), sleeping bandits (Nguyen and Mehta, 2024), and costly generative action sets (Xu et al., 2026) already address important forms of changing availability. We do not claim that growth, generation, or counterfactual response alone is new. The focus here is the formal transfer between complete executions and the local conditions under which its error can be controlled. These references provide context, not unproved imported premises of the numbered results. Appendix I A fully specified native reflection instance This appendix proves Corollary 12 without changing the general theorems. It provides a mathematical existence witness, not a measurement of a deployed language model. The instance is deliberately validation-dominant. A complete validator identifies a useful program, so the native controller can use it without learning an external selection rule. Generation can nevertheless fail, the registered library genuinely grows, deployment has a nonzero discrepancy, and all operation prefixes respect the same hard budget. The reference Bandit is used only in the proof. The construction does not establish joint tightness of all terms in the general bound. Scope of the instance. The guarantee concerns the specified frozen template generator, complete validator, retention rule, native schedule, and localized deployment check. The no-regret conclusion is along a horizon-parameterized family, rather than a single anytime controller. Applying this design pattern to a language-model agent requires establishing the corresponding generation, validation, retention, resource, and deployment conditions for that agent. The example establishes joint feasibility of the native-transfer interfaces and a concrete benefit of reflection within this model. I.1 Tasks, programs, and the frozen reflection mechanism Fix integers k,N≥1k,N≥ 1 and T=k+NT=k+N. Task t presents xt∈0,1x_t∈\0,1\ and requests the program output xtx_t. The context sequence can be fixed arbitrarily before execution. A structured result records the answer, program identity, validation status, and remaining resources. The common task scorer is zero for the correct answer and one otherwise. It is applied identically to the learner and every comparator. There are three immutable program identities. Their executable content is P0(x)=x+1,P1(x)=x+2,P2(x)=x.P_0(x)=x+1, P_1(x)=x+2, P_2(x)=x. (88) Initially only P0,P1P_0,P_1 are registered. A complete validator tests both inputs, so it accepts P2P_2 and rejects the other two for this specification. This is possible because the template family and task domain are finite. We do not assume that finite tests establish correctness for arbitrary programs. The fixed reflection kernel supports two prompts. A generic repair prompt returns P2P_2 or P1P_1 with equal probability. A guided template prompt returns P2P_2 deterministically. These are two specified input modes of the same unchanged kernel, available to both learner and comparator. The native learner uses the generic prompt. The comparator below uses the guided prompt. No learned weight, success probability, or hidden optimal-card label is supplied to the native controller. After each of the first k completed tasks, the native learner makes one generic generation and validation attempt. Every successful candidate is registered immediately unless its immutable identity is already present. The controller retains the success flag and uses P0P_0 throughout this prescribed preparation phase. Thus early registration does not force immediate execution. After the kkth attempt, it executes P2P_2 if present and P0P_0 otherwise. This batching choice incurs an explicit k-task acquisition cost. It is a behavior of this particular controller, not a restriction on the rapid-registration interface. Ordinary execution and execution with an additional check are legal runtime operations for every procedure. On the first subsequent task only, the native schedule invokes the check, which drops a successful output with probability 1/41/4, replacing it by the fallback answer. Its private bit is not retained in memory or the structured result. It does not modify registered programs, future tasks, or the future control rule. Later tasks execute the retained program normally. The clean reference performs the same charged check but leaves the output unchanged, so both resource counters agree. The native controller is consequently neither the reference Bandit nor identical to its own clean deployment. I.2 Own-history comparators and prefix resources The comparator class ℳ0M_0 contains two procedures. Procedure μ0 _0 always uses P0P_0. Procedure μ1 _1 makes one guided generation, validates and registers its output before the first task, and then uses P2P_2. Pre-task internal operations are legal for both procedures and the learner. The native learner simply follows its prescribed later schedule. The environment and scoring rule are unchanged. Consequently JT(μ0)=T,JT(μ1)=0,infμ∈ℳ0JT(μ)=0.J_T( _0)=T, J_T( _1)=0, _μ _0J_T(μ)=0. (89) These are separate counterfactual executions, not comparator actions evaluated against the native memory. Nonnegative scores also imply that adding other legal comparators cannot lower this infimum below zero. The two-element class is sufficient for the formal witness. Each attempt is charged two units at initiation, one for generation and one for its validation. Registration of the new identity consumes one further unit, and the deployment check consumes one unit. Initial registrations are part of the common initial condition. If r attempts have been initiated and u,v∈0,1u,v∈\0,1\ indicate whether registration and the check have been charged, every native prefix satisfies Cr=2minr,k+u+v≤2k+2.C_r=2 \r,k\+u+v≤ 2k+2. (90) The guided comparator costs three units, at most 2k+22k+2. The fallback comparator costs zero. Upfront charging also covers prefixes inside an unfinished attempt. Failed attempts are not refunded. Resource charges restrict admissibility and are not added again to the task scorer. The separate local deployment resource is one check, so its activity budget is BA=1B_A=1, while BC=0B_C=0. I.3 The native probability law and actual task losses Let Hk=(ζ1,…,ζk)∈0,1kH_k=( _1,…, _k)∈\0,1\^k be the generic trial outcomes, with success encoded by one. For a prefix hjh_j, the conditional next-outcome probability is 1/21/2 for either value. The resulting finite law is the recursively normalized product law, not an assumed expected-loss formula. Define ξ(h)=ζ1=⋯=ζk=0,ℙ(ξ(Hk)=1)=2−k.ξ(h)=1\ _1=·s= _k=0\, (ξ(H_k)=1)=2^-k. (91) The deployment bit D has probabilities ℙ(D=1)=1/4P(D=1)=1/4 and ℙ(D=0)=3/4P(D=0)=3/4, independently of the trial history. Pre-sampling these bits is only a representation of the law. Decisions access each trial result after its generation and the deployment bit only at its check. For each realized (h,d)(h,d), the completed-task loss is Yt(h,d)=1,0≤t<k,ξ(h)+t=k,d=1(1−ξ(h)),k≤t<T.Y_t(h,d)= cases1,&0≤ t<k,\\ ξ(h)+1\t=k,\ d=1\(1-ξ(h)),&k≤ t<T. cases (92) All scores lie in [0,1][0,1]. Summing this actual process before taking expectations gives ∑t<TYt(h,d)=k+Nξ(h)+d(1−ξ(h)),JT(A)=Hk[k+Nξ(Hk)+14(1−ξ(Hk))]. _t<TY_t(h,d)=k+Nξ(h)+d(1-ξ(h)), J_T(A)=E_H_k [k+Nξ(H_k)+ 14(1-ξ(H_k)) ]. (93) The Lean declarations task_sum, conditional_execution, and execution_identity establish this correspondence. Thus the expected loss is derived from task execution rather than introduced as an unconstrained endpoint. I.4 Local generation and full-state deployment conditions Each unsuccessful trial history has conditional success probability ρ=1/2ρ=1/2. A successful card is correct on every subsequent task and is retained. Therefore δ=0δ=0. The available post-preparation path uses P2P_2 when generated and a fallback otherwise. Its difference from the ideal comparator path is Nξ(Hk)Nξ(H_k). Applying the existing local-generation theorem gives G=Hk[Nξ(Hk)]≤N2−k.G=E_H_k[Nξ(H_k)]≤ N2^-k. (94) Here the episode delay is zero because the entire preparation loss is already charged as F=kF=k. Charging another k in G would duplicate the same loss. The exact failure probability follows as well by induction on the independent binary trials. At the deployment check, the future-relevant state consists of the retained success flag, the output-failure bit, and the deterministic task and resource counters. The registered library is determined by the success flag. Raw historical records can also be retained, but neither kernel uses the past output bit in a future decision. The native and clean kernels preserve the same memory and counters. Their complete stochastic state distributions have TV(K,L)=14(1−ξ(h)).TV(K,L)= 14(1-ξ(h)). (95) After that task they induce identical future control and losses. Conditional on the completed prefix h, the retained memory is fixed and the future loss is common to both output branches. Their continuation-value span is at most one. The local discrepancy is at most 1/41/4 and the check costs one unit. Averaging the resulting conditional difference, or directly using equation 93, gives the deployment certificate EA≤1⋅14⋅BA=14,EC=0.E_A≤ 1· 14· B_A= 14, E_C=0. (96) The formalization computes TV on the joint memory-output state, proves that later task scores ignore the slip bit, and establishes the exact endpoint difference. The span-one statement is conditional on the fixed memory, not a global span assertion across successful and unsuccessful memories. Those memories can have very different future values. This instance therefore supplies the deployment edge of Theorem 7 directly. It does not assume the stronger global range contract of Theorem 9 with H¯=1 H=1 on the unconditioned mixed-memory state space. I.5 The reference Bandit and the native selection bridge Condition on a completed generation history h, before drawing any reference action. Consider a two-arm reference pool. Arm zero is P0P_0. Arm one is P2P_2 if available, and otherwise P1P_1. These are distinct immutable identities in either case. The unused registered fallback need not enter this comparison pool. Registration is causal because the reference experiment begins after the k attempts. The native registered library grows on every successful trial trajectory, even though the subsequent comparison pool has two members. The reference algorithm initializes both probabilities at 1/21/2 and performs ordinary exponential weighting with learning rate η>0η>0 and identity transition. Only the selected score enters the update. Its score is ℓh(0)=1,ℓh(1)=ξ(h),qr(i)=1. _h(0)=1, _h(1)=ξ(h), q_r(i)=1. (97) The observation kernel is deterministic conditional on the selected identity. It therefore satisfies the accepted-score identity exactly. Positivity of exponential weights gives full support at every finite time. The comparator path is arm one, with code C=log2C= 2 and no switches. The standard conditional second-moment calculation gives Vest≤2NV_ est≤ 2N. The constructed Lean Program recursively generates its draw probabilities and observations. Its capacity and code conditions are proved, not supplied as assumptions. Let Jsel(h)J_ sel(h) be its expected post-preparation loss and Jav(h)=Nξ(h)J_ av(h)=Nξ(h). Both arms have loss at least ξ(h)ξ(h), so Nξ(h)≤Jsel(h),Jsel(h)−Nξ(h)≤log2η+ηN.Nξ(h)≤ J_ sel(h), J_ sel(h)-Nξ(h)≤ 2η+η N. (98) The first inequality is the crucial native bridge. The clean native controller has total loss k+Nξ(h)k+Nξ(h), hence its acquisition edge is at most k. This is a one-sided performance comparison proved from validation, not an assertion that native sampling probabilities equal the Bandit probabilities. On a successful history, the native clean controller always uses the correct card. The initial reference draw uses the fallback with probability 1/21/2, and the deployed native controller uses it with probability 1/41/4 on its first post-preparation task. The controllers are genuinely distinct. I.6 A causal coupling with the correct native marginal Write wk(h)w_k(h) for the recursively generated trial probability, s(d)s(d) for the deployment-bit probability and Qη,h(g)Q_η,h(g) for the law of a complete N-slot reference trajectory. The latter law comes from the constructed Bandit recursion, not from native action logs. On the finite product space define Γ(h,d,g)=wk(h)s(d)Qη,h(g),∑h,d,gΓ(h,d,g)=1. (h,d,g)=w_k(h)s(d)Q_η,h(g), _h,d,g (h,d,g)=1. (99) Each factor is nonnegative and normalized at its proper stage. The reference uses h only after all k trials have completed. It does not use the subsequent deployment bit. Thus this conditioning does not reveal future generation outcomes to an earlier draw. The native output functional in equation 92 does not depend on g. Marginalizing the freshly generated reference path gives ∑h,d,gΓ(h,d,g)∑t<TYt(h,d)=∑h,dwk(h)s(d)∑t<TYt(h,d)=JT(A). _h,d,g (h,d,g) _t<TY_t(h,d)= _h,dw_k(h)s(d) _t<TY_t(h,d)=J_T(A). (100) Both comparators have deterministic scores on their own executions, so they can be coupled to this space without changing either native law. The learner marginal is the same for both comparator choices. The Lean declarations joint_law_normalized and native_marginal prove these identities using normalization of the actual reference recursion. This supplies the compatibility missing from a comparison of isolated action marginals. I.7 All certificates in one experiment For the best comparator μ1 _1, set all ideal comparator-side endpoints to zero. This is its actual loss, represented exactly by P2P_2, whether or not that program is available to the learner. The available-to-ideal difference is precisely the generation edge. The fallback comparator has nonnegative loss, so the same final upper bound applies to it. No learner marginal depends on this comparator choice. Use one task per reference slot, no response contamination and no path switches. In the notation of Theorem 7, the proved common budgets are b=1,S=hresp=Nb=0,C=log2,V=2N,F=k,G=N2−k,EA=14,EC=DA=DC=Enf=0. gatheredb=1, S=h_resp=N_b=0, C= 2, V=2N,\\ F=k, G=N2^-k, E_A= 14, E_C=D_A=D_C=E_ nf=0. gathered (101) Generation cost constrains equation 90. The preparation task loss appears only in F. Failed post-preparation opportunities appear only in G. The deployment check appears only in EAE_A. Exact validation and the absence of an endogenous environment state make the remaining edges zero by construction, not by a generic assumption about reflective agents. Apply the unchanged native-transfer theorem conditionally on h, using the actual reference recursion. Then average over the normalized generation law and use the local-generation theorem. Equation equation 89 identifies the own-history comparator infimum. This proves RT(A,ℳ0)≤k+N2−k+14+log2η+ηN.R_T(A,M_0)≤ k+N2^-k+ 14+ 2η+η N. (102) In Lean, conditional_main invokes ModelMain.finite_controller_transfer. The declaration instantiated_bound averages that theorem and invokes generation_bound. The proof therefore uses the existing selection and transfer chain rather than merely proving a numerically similar inequality in isolation. I.8 The horizon-indexed family and its scope For k=n+1k=n+1, put N=k2N=k^2, T=k2+kT=k^2+k and η=1/kη=1/k. Equation equation 102 becomes the first inequality in Corollary 12. Induction gives k≤2k≤ 2^k, hence k22−k≤k^22^-k≤ k. Since k2≤Tk^2≤ T, this is an O(T)O( T) bound along the specified horizons. More explicitly, RT(A,ℳ0)T≤2+log2k+2−k+14k2⟶0. R_T(A,M_0)T≤ 2+ 2k+2^-k+ 14k^2 0. (103) The positive-part limit is checked in Lean. Without reflection, μ0 _0 has regret exactly T, so the construction is not a comparison against the learner itself. It is an existence result for a restricted verified-template model, not an optimal-rate theorem, an arbitrary-language-model guarantee, or a single horizon-free controller. The constant coverage and complete validator are strong, explicit structural features. Removing them requires additional analysis. The model nevertheless demonstrates that genuine rule generation, retained native control, nonzero deployment error and hard resource feasibility can coexist with the unchanged theorem and a nonvacuous sublinear conclusion. Appendix J Joint generation quality and hard resources This appendix proves Corollary 13. The existing transfer theorem is unchanged. The new step couples the required policy quality to conditional coverage, trial quotas, and actual hard resources. A fixed design determines these parameters and a causal trial schedule. Selecting a design for a horizon does not replace the native controller by a Bandit controller. The guarantee applies when that native procedure satisfies the stated interfaces for the selected design. J.1 Contracts and the meaning of the parameters Fix a comparator before execution. For episode e, quality tolerance δe _e bounds the conditional expected available-minus-aligned task gap after success. A success means that a comparator-suitable rule has been generated, validated, retained, and made causally usable. It is an analysis predicate, not an optimal-policy label supplied to the native procedure. The lower bound ρe(δe)∈(0,1] _e( _e)∈(0,1] must hold after every still-unsuccessful trial history. Improving the requested quality may decrease this bound. A separate statement about text quality alone would not imply the task-gap contract. The quota ke∈ℕk_e bounds attempted generation and validation operations. Successful episodes may stop early, with inactive trials padded for analysis. Such padding consumes no additional resource and cannot undo a success. The worst-case per-attempt envelope ce(δe)c_e( _e) includes failures. Costs outside this envelope, such as registration, are included in BTotherB_T other. The plan is fixed before play, though its trial kernels and legal decisions may depend on completed history. Random redesign of the quotas requires a separate predictable-envelope argument. Episode slots refer to one learner schedule shared by all comparator analyses. Success predicates may depend on the comparator, but the same physical attempt is charged once. Resource costs are not summed over counterfactual comparators. The common plan supplies uniform envelopes for their separate generation-gap proofs. For a legal learner prefix h, let ue(h)u_e(h) be its initiated attempt count and Cother(h)C other(h) its remaining charged costs. Assume each attempt reserves its cost before unfinished internal work can violate a budget, all costs are nonnegative, ue(h)≤keu_e(h)≤ k_e, and Cother(h)≤BTotherC other(h)≤ B_T other. Then CA(h)≤Cother(h)+∑eue(h)ce(δe)≤BTother+∑ekece(δe)≤BT.C_A(h)≤ C other(h)+ _eu_e(h)c_e( _e)≤ B_T other+ _ek_ec_e( _e)≤ B_T. (104) This proves every-prefix hard feasibility, including prefixes inside a failed or unfinished attempt. It does not replace the comparator admissibility definition. Each comparator still executes on its own history and satisfies its own original hard constraint. In particular, a comparator cannot borrow a card or unused resource from the learner. These resource costs constrain execution rather than adding a second loss penalty. J.2 Conditional failure, task gaps, and native regret Let Fe,jF_e,j be the event that the first j trials in episode e have not succeeded, and let ℱe,jF_e,j record those completed trials. Under the actual episode law ℙeP_e, conditional coverage implies ℙe(Fe,j+1)=ℙe[Fe,jℙe(Fe,j+1∣ℱe,j)]≤[1−ρe(δe)]ℙe(Fe,j).P_e(F_e,j+1)=E_P_e\! [1_F_e,jP_e(F_e,j+1 _e,j) ]≤[1- _e( _e)]P_e(F_e,j). (105) The first equality uses that Fe,j+1⊆Fe,jF_e,j+1 F_e,j and the tower rule. On a successful history the indicator is zero. On an unsuccessful history the conditional failure probability is at most 1−ρe(δe)1- _e( _e). Starting from probability one and applying this argument kek_e times gives ℙe(Fe,ke)≤[1−ρe(δe)]ke≤exp−keρe(δe).P_e(F_e,k_e)≤[1- _e( _e)]^k_e≤ \-k_e _e( _e)\. (106) For the second inequality, 1−x≤e−x1-x≤ e^-x for x∈[0,1]x∈[0,1], both sides are nonnegative, and raising to the nonnegative integer power preserves order. No independence assumption was introduced. On every completed generation history, the conditional expected per-task gap is bounded by one during the τe _e delay tasks and by δe+Fe,ke _e+1_F_e,k_e for the nen_e subsequent tasks. Integrating under the same episode law gives ℙe[∑t<τege,tpre+∑t<nege,tpost]≤τe+ne[δe+e−keρe(δe)].E_P_e [ _t< _eg pre_e,t+ _t<n_eg post_e,t ]≤ _e+n_e [ _e+e^-k_e _e( _e) ]. (107) The random variables ge,tpreg pre_e,t and ge,tpostg post_e,t are conditional task-gap functions on completed trial histories, as in Appendix E. Their sums must represent the actual available-to-aligned endpoint difference. Summing these identities and bounds establishes the generation certificate. Uniformity over the original comparator class permits the counterfactual infimum in Theorem 7. Its remaining certificates, reference selection theorem, and own-law realizations are unchanged. Substitution proves equation 24. The quantity U¯T U_T contains all remaining reference and deployment terms. In particular, direct deployment certificates and those proved by Theorem 9 are both admissible. Replacing a direct certificate with a local proof does not create an additional copy of the same endpoint difference. Likewise, a preparation delay already charged in F has zero additional delay in equation 107. In Theorem 9, local shift εt _t is weighted by downstream sensitivity hth_t, along the actual law ℙKP_K. Resource use limits the accumulated charge, not the union of all possible reflection times. Bounded card lifetime alone does not bound hth_t, since descendants and environment changes can retain the effect. For the asymptotic claim, the uniform envelopes in the corollary give RTT≤U¯T+∑eτeT+δT+e−λT. R_TT≤ U_T+ _e _eT+ _T+e^- _T. (108) The right side tends to zero. Continuity of the positive-part map and the nonnegative lower bound on max0,RT/T \0,R_T/T\ yield the claimed limit. This argument derives a regret bound from native execution witnesses before taking a limit. It does not assume that regret itself is sublinear. A vanishing coverage probability is allowed, provided cumulative exposure keρe(δe)k_e _e( _e) still diverges uniformly. Increasing kek_e alone does not establish this property. J.3 Explicit quotas and a polynomial quality-cost family For a desired log-failure level Λ>0 >0, a coverage lower bound ρ⋆>0 _ >0, and per-attempt cost envelope c⋆≥0c_ ≥ 0, define k=⌈Λρ⋆⌉,kρ⋆≥Λ,kc⋆≤(Λρ⋆+1)c⋆.k= _ , k _ ≥ , kc_ ≤ ( _ +1 )c_ . (109) The first bound follows from ⌈x⌉≥x x ≥ x. The second follows from ⌈x⌉<x+1 x <x+1 for x≥0x≥ 0, weakening the strict inequality when c⋆=0c_ =0. Equations equation 106 and equation 109 bound the failure probability by e−Λe^- . A design can therefore check hard feasibility using these explicit quotas, including the integer-rounding cost. One illustrative class has constants ag∈(0,1]a_ g∈(0,1], c0>0c_0>0, integer exponents dg,dv≥0d_ g,d_ v≥ 0 with ν=dg+dv>0ν=d_ g+d_ v>0, and, uniformly over episodes and comparators, ρe(δ)≥agδdg,ce(δ)≤c0δ−dv,0<δ≤1. _e(δ)≥ a_ gδ^d_ g, c_e(δ)≤ c_0δ^-d_ v, 0<δ≤ 1. (110) The exponent dgd_ g describes how quickly suitable candidates become rare as quality improves. The exponent dvd_ v describes increasing generation or validation cost. These are additional properties of this illustrative class, not new assumptions imposed on every model in the main theorem. Integer exponents suffice for this formally checked example. Choose ρ⋆=agδdg _ =a_ gδ^d_ g and the quota in equation 109. Since δdg≤1δ^d_ g≤ 1, the cost of all attempts in any episode satisfies kce(δ)≤(Λagδdg+1)c0δdv=c0(Λ/ag+δdg)δν≤c0(Λ/ag+1)δν.kc_e(δ)≤ ( a_ gδ^d_ g+1 ) c_0δ^d_ v= c_0( /a_ g+δ^d_ g)δ^ν≤ c_0( /a_ g+1)δ^ν. (111) Let ET≥1E_T≥ 1 be the deterministic number of episode slots, including padding, and let bTgen>0b_T gen>0 be the allocation for these attempts after reserving other costs. This is a resource allocation, distinct from the run cap b. Define zT=c0ET(Λ/ag+1)bTgen,0<zT≤1,δT=zT1/ν.z_T= c_0E_T( /a_ g+1)b_T gen, 0<z_T≤ 1, _T=z_T^1/ν. (112) The positive real root satisfies 0<δT≤10< _T≤ 1 and δTν=zT _T^ν=z_T. Substituting into equation 111 and summing the ETE_T slots bounds total attempt cost by bTgenb_T gen. Hence bTgen+BTother≤BTb_T gen+B_T other≤ B_T ensures the original hard constraint. This is a sufficient, explicit design, not an infimum over incompatible parameter choices. For T≥2T≥ 2, take Λ=2logT =2 T. Then e−Λ=T−2e^- =T^-2, and the aggregate failure contribution is at most T−1T^-1 when ∑ene≤T _en_e≤ T. Thus equation 108 specializes to RTT≤U¯T+∑eτeT+[c0ET(2logT/ag+1)bTgen]1/ν+T−2. R_TT≤ U_T+ _e _eT+ [ c_0E_T(2 T/a_ g+1)b_T gen ]^1/ν+T^-2. (113) If the bracketed ratio tends to zero, the quality term tends to zero by continuity of a positive power at zero. Remaining terms must still vanish. For fixed ag,c0a_ g,c_0, the familiar sufficient scaling ETlogT=o(bTgen)E_T T=o(b_T gen) makes that ratio vanish. When additional delay and deployment effects are bounded by a fixed constant times bTgenb_T gen, one also chooses bTgen=o(T)b_T gen=o(T) and verifies the unaffected reference terms. Resource availability itself need not be sublinear, since an agent need not spend its entire allowance. The values of coverage and cost envelopes determine this design. An algorithm adapting to unknown envelopes is a further learning problem, not a consequence of taking an infimum over designs. Any such optimization must retain the dependence of delay, observation, switching, and deployment terms on the same design. J.4 Compatibility with the native verified-template instance Corollary 12 and Corollary 13 use the same transfer theorem with different choices of the local generation parameters. In the verified-template instance, there is one episode with ke=k_e=k, ne=Nn_e=N, ρe(0)=1/2 _e(0)=1/2, and δe=0 _e=0. A trial costs two units, and registration plus the deployment check reserve two further units. The hard bound is exactly 2k+22k+2. Preparation is already charged as F=kF=k, so τe=0 _e=0 in the generation ledger. Its direct deployment charge remains 1/41/4. The generic exponential failure envelope becomes e−k/2e^-k/2. The exact finite-model probability is 2−k2^-k and is sharper. Keeping that exact bound preserves Corollary 12 verbatim. Its native controller and counterfactual comparators are unchanged. In particular, the new result does not demand the stronger global continuation-range contract discussed in Appendix I. The Lean declaration concrete_compatibility checks both conclusions on the original model. It retains the actual prefix-cost function and derives the exponential-envelope regret bound from the already proved native regret. Thus compatibility includes the concrete execution and hard resources, rather than only a comparison of abstract rate expressions. The polynomial specialization concerns δ>0δ>0 and illustrates a genuine precision-cost tradeoff. The existing exact-repair point has δ=0δ=0 and uses the more general corollary directly, rather than substituting zero into a negative-power cost formula. This distinction is the reason the two results are compatible. One establishes a nonempty concrete native model, while the other explains how a family of legal designs can allocate resources as quality requirements change. Formal proof chain. Module JointGenerationBudget reuses the normalized finite trial law and proved failure recurrence. It constructs the missing generation certificate from episode kernels and exact endpoint identities, then calls NativeFamily.own_coupling_counterfactual. Direct or locally established deployment certificates remain explicit inputs. Its variable-domain family theorem invokes this native endpoint before proving the limit. Separate declarations verify every-prefix costs, integer quotas, polynomial costs, logarithmic failure targets, and positive-root choices. The scalar power manipulations are supporting steps rather than substitutes for the native semantic connection. Interpretation of local generation reliability. Local generation reliability gives ℙe(ξe=1)≤(1−ρe)keP_e( _e=1)≤(1- _e)^k_e by successive conditional failure bounds. Integrating task gaps and summing episodes proves equation 20. More trials reduce failure, better retained policies reduce quality error, and faster acquisition reduces delay. Theorem 11 combines these effects with both deployment bounds and the remaining contracts. The Lean family endpoint applies this completed-task bound before taking the no-regret limit. Appendix E supplies the proof. All trials consume resources, including failures. Delay is charged here or in F, never both. Local generation reliability must hold uniformly over the comparator class. Increasingly precise, disjoint targets need not retain constant coverage. The remaining contracts must hold jointly. Appendix K Notation, types, and correspondence to the formal model The notation follows the usual distinction between losses ℓ , loss estimates ℓ , unnormalized weights w, and sampling probabilities p in online learning (Lattimore and Szepesvári, 2020; Mourtada and Maillard, 2017). A bold v is a path, never its loss. The functions JTJ_T and J with semantic superscripts denote expected totals, whereas L denotes a realized total. The separately defined JrJ_r is a sampled reference identity, not a loss. Subscripts and superscripts distinguish the native model, reference slots, local stability model, and binary benchmark. Dummy variables in explicitly local proofs are not additional global model parameters. K.1 Histories, probability laws, and conditioning An operation history h∈ℋsoph _s op records s completed internal operations. A task history Ht∈ℋttaskH_t _t task contains the initial record and t completed task records. These are not the same prefix space. A task-record kernel packages the internal computation between task boundaries, assuming it terminates and induces a measurable kernel. The theory does not prove termination of arbitrary language-model programs. The symbol E in Definition 1 is an admissibility relation, whereas E is expectation. The runtime is the mechanism that interprets a selected card, invokes tools or primitive actions, and updates the recorded state. A card kernel πi(da∣x,m) _i(da x,m) assigns a probability measure to actions a, conditional on context x and memory m. Here dada is integration notation, not a product involving an undefined parameter d. The same convention applies to the operation kernel μ(du∣h)μ(du h). For a measurable function f, execution averages f(a)f(a) as ∫f(a)πi(a∣x,m) f(a) _i(da x,m). For a fixed comparator, Γμ _μ is a joint proof law on a space Ωμ _μ. A realization is a measurable map from that space to a complete trajectory. The subscript #\# is the measure-pushforward operator, not a cardinality symbol. For a measurable trajectory event D, ((rA)#Γμ)(D)=Γμ(rA−1(D))((r_A)_\# _μ)(D)= _μ(r_A^-1(D)), where rA−1(D)=ω∈Ωμ∣rA(ω)∈Dr_A^-1(D)=\ω∈ _μ r_A(ω)∈ D\. Thus the probability of D is obtained by measuring the source outcomes mapped into it. The required equalities (rA)#Γμ=ℙA(r_A)_\# _μ=P_A and (rμ)#Γμ=ℙμ(r_μ)_\# _μ=P_μ preserve the complete native trajectory distributions, not merely one-step action marginals. The learner law ℙAP_A cannot change with the comparator used to prove the bound. The notation Jr,Or|hrE_J_r,O_r h_r means a finite conditional expectation under masses pr(i)kr(i,o)p_r(i)k_r(i,o) after fixing the completed pre-draw history. Equivalently, in a compatible reference process it is conditional expectation given ℱr−F_r^-. The sigma-field is generated by the completed prefix and contains no current draw or future observation. All slot-dependent objects may be functions of that prefix. The notation suppresses these arguments but does not assert determinism. By contrast, ΓμE_ _μ integrates the entire coupled experiment, including its random prefixes. The law ℙstop(r)P_ stop^(r) is a prefix marginal of the recursively generated stopped law. It is not conditioning on the terminal stopping time. The endpoint ℓrref(i) ^ref_r(i) is fixed before the current draw. Operationally it is the expected task-loss total obtained from the specified reference execution at that prefix and identity. The score yr(i,o)y_r(i,o) is an observable proxy. Equation equation 5 is a calibration assumption relating that proxy to the independently specified target. Defining the target to be an accepted-score average after the fact would not establish correspondence to task loss. Neither a positive qr(i)q_r(i) nor a positive sampling probability pr(i)p_r(i) supplies that correspondence. Table 3: Semantic and algorithmic notation. Domains and probability laws are part of the definitions. Symbol Meaning and scope T,t,s,r,R,NT,t,s,r,R,N Task horizon and task index, internal-operation index, reference-slot index, last padded slot, and slot cap N=R+1N=R+1. Defined in Sections 2 and 2.4. ,,(h), U, O, U(h), E Operation and result spaces, legal next operations, and admissible extension relation. These describe operational legality, not resource penalties. ,, X, M, A Context, memory, and primitive-action spaces. Lowercase x,m,ax,m,a are their elements. The benchmark phase count m is local to Section 4. ℋsop,ℋttaskH_s op,H_t task Operation-history and task-history spaces. Random task prefix Ht=(Z0,…,Zt)H_t=(Z_0,…,Z_t), with Zt∈tZ_t _t. Lowercase h is a realized history. πi,μ,A,μA,ℳ _i,μ,A, _A,M Execution-card action kernel, comparator meta-policy, complete native learner, its operation-selection kernel, and nonempty comparator class. i is immutable executable identity, not a primitive action. σt,Yt,LT,JT,RT _t,Y_t,L_T,J_T,R_T Common task scorer, scalar task loss, realized cumulative loss, expected cumulative loss, and own-history regret from equation 1. Unqualified RTR_T abbreviates RT(A,ℳ)R_T(A,M). ℙA,ℙμ,ΓμP_A,P_μ, _μ Own-trajectory laws and comparator-specific coupling with the prescribed native marginals. Ωμ,ω _μ,ω denote its sample space and outcome. rA,rμ,(rA)#Γμr_A,r_μ,(r_A)_\# _μ Measurable trajectory realizations and the induced trajectory law. The subscript #\# denotes measure pushforward. The letter r alone indexes a reference slot. Costtμ,BtCost_t^μ,B_t Cumulative resource use and deterministic hard budget at task boundary t. Non-task operationwise restrictions must be imposed separately. ℱr−,hr,ℐrF_r^-,h_r,I_r Pre-draw sigma-field, realized completed prefix, and nonempty finite available identity set. The set and local kernels may be history-dependent. r active1\r active\ Indicator that the reference process has not terminated and the completed history permits slot r. It is ℱr−F_r^--measurable, not a card-availability or feedback-acceptance indicator. νr,wr,Wr _r,w_r,W_r Probability prior, nonnegative unnormalized weight vector, and total weight Wr=∑iwr(i)>0W_r= _iw_r(i)>0. WrW_r is not a task record ZtZ_t. pr,Jr,Θr,αp_r,J_r, _r,α Sampling probability vector, sampled reference identity, row-stochastic sharing transition, and share rate in (0,1)(0,1). The general transition need not use the Fixed-Share specialization. kr,Or,Mr,qrk_r,O_r,M_r,q_r Conditional outcome kernel, random outcome, binary acceptance mask, and acceptance probability conditional on the selected identity. qrq_r is not the probability of selecting that identity. λr,yr,dr,ℓrref _r,y_r,d_r, ^ref_r Reference task-loss total, observed proxy score, its predictable upper bound, and reference expected loss per identity. Equation equation 5 links the two scores. ℓ^r,er _r,e_r Importance-weighted estimated loss and zero-conditional-mean learner–comparator estimation noise. Squaring a vector means coordinatewise squaring. μ,vr,C(),Cv^μ,v_r,C(v),C Predictable available comparator path, its identity coordinate, realized negative log path mass, and deterministic uniform code bound. Dependence on μ is suppressed locally. Vest,V_ est,V Raw cumulative second-moment budget in equation 11 and its scaled envelope with Vest≤bV_ est≤ bV. Neither is a centered variance. ℙstop,ϖr,Fr,frP_ stop, _r,F_r,f_r Stopped law, completed-prefix probability mass, cumulative event score, and its one-step increment in Appendix B. FrF_r there is not the scalar foreground budget F. ωr _r^v Unnormalized contribution of a single supported path to weight wr(vr)w_r(v_r), as defined in equation 47. K.2 Endpoint types and the single accounting chain Fix T and μ. Each intermediate endpoint is an explicitly chosen integrable score random variable on the coupling space. Its expectation is the displayed scalar J. The superscripts describe its role, not an algebraic operation that could manufacture the endpoint automatically. An application must supply the random variables and their semantic identifications before proving their inequalities. In particular, JμavJ_μ^av is an expected score, whereas v is a random predictable path. Table 4: Expected endpoints, directed charges, and exact Lean field names. All expectations use Γμ _μ. Endpoint or charge Definition, outgoing comparison, and correspondence JAnatJ_A^nat Expected native learner loss JT(A)J_T(A). Expectation of realA. Its difference from JArefJ_A^ref is bounded by EAE_A. JArefJ_A^ref Expected reference learner endpoint, expectation of refA. Its difference from JselJ^sel is bounded by F+b+DAF+P_b+D_A. JselJ^sel ∑r=0RΓμℓrref(Jr) _r=0^RE_ _μ ^ref_r(J_r), identified with Experiment.selectedTotal. Its comparison to JμavJ_μ^av is the proved selection bound. JμavJ_μ^av ∑r=0RΓμℓrref(vr) _r=0^RE_ _μ ^ref_r(v_r), identified with Experiment.availableTotal. Its difference from JμalJ_μ^al is bounded by G. JμalJ_μ^al Aligned represented comparator score, expectation of aligned. Its difference from JμclJ_μ^cl is bounded by bSbS. JμclJ_μ^cl Score after removing alignment, expectation of clean. Its difference from JμpathJ_μ^path is bounded by hresp(S+1)+DCh_resp(S+1)+D_C. JμpathJ_μ^path Reference execution-path score after response comparison, expectation of refPath. Its difference from JμrefJ_μ^ref is bounded by EnfE_ nf. JμrefJ_μ^ref Reference comparator meta-policy score, expectation of refM. Its difference from JμnatJ_μ^nat is bounded by ECE_C. JμnatJ_μ^nat Expected native comparator loss JT(μ)J_T(μ), expectation of realM. No outgoing arrow is needed. EA,EC,EnfE_A,E_C,E_ nf Learner deployment, comparator deployment, and representation budgets, corresponding to Budget.E_cpA, E_cpC, E_nf. F,G,DA,DCF,G,D_A,D_C Foreground-displacement, generation, learner-calibration, and comparator-calibration budgets. The Lean Budget fields have these same names. b,hresp,Nb,S,Vb,h_resp,N_b,S,V Nominal run cap, response-bound scale, extra-boundary envelope, path-switch envelope, and scaled capacity. Lean fields are b, H, N, S, V. In particular, Budget.N is NbN_b, not the slot cap N. b,Δ,UTP_b, ,U_T Prefix allowance, sum of seven scalar charges, and final upper bound, matching Budget.prefix, delta, and bound. gTgen(μ),Gg_T gen(μ),G Exact signed endpoint difference Jμav−JμalJ_μ^av-J_μ^al and a uniform upper budget. Their relationship is gTgen(μ)≤Gg_T gen(μ)≤ G, not equality by definition. The seven directed certificates in equation 13 are not seven independently optimized regret objectives. Together with the proved selection arrow they form the eight adjacent differences in equation 50. The scalar budgets may be signed when a tighter directed comparison permits it. The local generation theorem constructs a nonnegative envelope. No sign assumption is used to telescope the endpoints. Nonnegative multipliers are required when substituting upper budgets, such as η/2η/2 for the capacity inequality. K.3 Local-model and benchmark notation Local generation reliability is the collective term for the success and task-quality conditions in Section 3.3. Success includes validation, retention, and causal usability. The parameters ρe _e and δe _e quantify these properties, while episode accounting and hard feasibility govern their composition. This term introduces no additional numeric parameter. Table 5: Notation specific to stability, generation, and the paid binary benchmark. Symbol Meaning and scope St,s,Kt,Lt,pinitS_t,s,K_t,L_t,p init Complete finite state, its realization, native and reference state-transition kernels, and common initial distribution in Section 3.2. The capital switch bound S is not a state. ct,Vt,nL,ht,H¯c_t,V^L_t,n,h_t, H Common immediate state score, n-step continuation value from state-time t, local continuation-range envelope, and its uniform bound. H¯ H is distinct from the response scale hresph_resp. TV,DKL,εt,ε¯TV,D_KL, _t, Total variation, relative entropy, local full-state TV envelope, and uniform activity-scaled TV factor. Relative entropy uses natural logarithms and the common support in Appendix F. χt,rt,cmin,BA,BC _t,r_t,c_ ,B_A,B_C Nonnegative update activity, actual-path resource charge, strictly positive cost per unit activity, and learner/comparator resource envelopes. Here rt(s)r_t(s) is a resource function, not a slot number. ζt,t,n,κ _t,D_t,n,κ Local product htεth_t _t, its accumulated K-Bellman charge, and H¯ε¯/cmin H /c_ . The proof integrates along the native K law. e,k,ke,ℋe,kgene,k,k_e,H_e,k gen Generation episode, trial index, number of trials, and episode-specific completed-trial space. Trials and task rounds need not coincide. ℙe,ϖkgen,gk,bk,ξkP_e, _k gen,g_k,b_k, _k Episode law, prefix mass, generation kernel, success indicator in 0,1\0,1\, and all-failed indicator. Episode index e is suppressed inside the one-episode proof. ρe,δe,τe,ne _e, _e, _e,n_e Conditional retained-card success lower bound, post-success quality tolerance, number of delay tasks, and number of later tasks in that episode. gtpre,gtpost,ξeg_t pre,g_t post, _e Conditional task-gap functions and failure indicator after kek_e trials. The first two are not the trial kernel gkg_k. Their episode sums identify the actual generation endpoint. AT,δT,fT,UTrestA_T, _T,f_T,U_T rest Uniform delay, quality, and failure envelopes, and the reference bound with G=EA=EC=0G=E_A=E_C=0. ATA_T is a numeric delay allowance, not the learner A. ρe(δ),ce(δ) _e(δ),c_e(δ) Quality-dependent conditional coverage and prepaid per-attempt resource upper bound in Corollary 13. BTother,CA(h)B_T other,C_A(h) Reserved other costs and total learner cost at legal prefix h. Cother(h),ue(h)C other(h),u_e(h) Other charged costs and episode attempt count at legal prefix h. U¯T,λT U_T, _T Full transfer bound with only G removed, and a uniform lower bound on exposure keρe(δe)k_e _e( _e). Fe,j,ℱe,jF_e,j,F_e,j No-success event after j trials and completed-trial information in episode e. The event Fe,jF_e,j is distinct from the foreground-loss budget F. Λ,ρ⋆,c⋆ , _ ,c_ Log-failure target, coverage lower bound, and trial-cost envelope for the explicit quota in equation 109. ag,c0,dg,dv,νa_ g,c_0,d_ g,d_ v,ν Polynomial coverage coefficient, cost coefficient, nonnegative integer exponents, and their positive sum in equation 110. ET,bTgen,zTE_T,b_T gen,z_T Episode-slot count, attempt-resource allocation, and dimensionless ratio defining the positive quality root. None is the run cap b or a deployment-error certificate. m,n,B,j,Kj,j(t)m,n,B,j,K_j,j(t) Public phase count, phase length, total integer registration budget, phase index, phase library size, and phase containing task t. The benchmark uses T=mnT=mn. ,ℓtbase,It,qD, _t base,I_t,q Legal loss-table domain, fixed binary base loss, emitted identity, and primitive observation probability. The score masks are independent Bernoulli variables with parameter q. ,,ItV,v,I_t^v Deterministic eligible phase paths, one such path, and its emitted identity. Unlike the native comparator, this benchmark comparator is a phase path on an oblivious table. ,ℛbin∗ A,R^*_ bin All causal randomized phase controllers and their minimax task regret in equation 27. ℙ0,ℙj,ϵ,NjP_0,P_j,ε,N_j Null and hidden-target observation laws, Bernoulli mean gap, and the number of draws of identity j in the finite lower-bound proof. ptlow,xj,yj,Eqp_t low,x_j,y_j,E_q Conditional learner kernel in that proof, null and target expected draw counts, and the independent-erasure map on distributions. r,ur,Xi,VphaseT_r,u_r,X_i,V_ phase Task-index set of a held run, its length, its corrected loss under identity i, and phase-level second-moment envelope. Phase calculations suppress their phase index. K.4 What the correspondence check does and does not establish The paper notation is deliberately not forced to reproduce every internal Lean variable. In DependentTransfer.Experiment, fields P, z, v, and V denote Θ , ℓ , v, and VestV_ est. Its measure parameter, locally named µ in mathematical presentations of the code, is the coupling law rather than a comparator meta-policy. The field R yields R+1R+1 scored slots. In FiniteObservation.Round, kernel, accepted, score, loss, and q correspond to k, M, y, ℓref ^ref, and q. The target loss is an input field and the accepted-score identity is a premise. An operational scorer λ supplies a target instance, not a new theorem that every log is calibrated. The native record convention follows CausalTrajectory.History, whose prefix includes coordinate zero. Task score t is evaluated after record t+1t+1, as in NativeSemantics.Execution.score. The resource class in ResourceClasses has T+1T+1 task-boundary prefix coordinates. It does not silently quantify over an unrelated number of internal operations. Local generation indicators are ordinary 0/10/1 values when multiplied, corresponding to Boolean tests with explicit coercion in the code. The companion includes proved correspondence results without adding a numbered paper theorem. The family endpoint explicitly permits horizon-dependent finite domains and uses the combined-resource limit in Theorem 11. The source-and-log audit checks the included declarations and their dependencies. The interpretation of the English model and its operational identifications is manually reviewed, not mechanically proved by renaming notation. Integrability and exact score-law identifications remain part of the stated contracts. The operational control kernel μA _A is not the literal type of NativeSemantics.Execution.controller. That Lean field is the induced task-record kernel after internal operations have been packaged together with their results and runtime effects. The interface assumes this packaging is well-defined. Renaming the operational kernel does not establish a new compiler-correctness theorem. K.5 Terminology conventions The reference algorithm denotes Algorithm 1, previously called a shadow algorithm. A reference experiment additionally specifies its probability law, scores, and comparator path. A proxy score is the observed scalar yry_r, not a second algorithm. A run is a scored execution interval, a slot is its reference decision index, and a generation episode groups attempts and associated task gaps. These units need not have equal lengths. The complete-execution objective RTR_T is called counterfactual regret to emphasize own-history policy-regret semantics. The signed generation opportunity gap gTgen(μ)g_T gen(μ) is one intermediate difference, and G is its upper bound. Neither is a newly introduced independent regret objective. A certificate is an explicit bound used by the proof, while Lean verification checks a conditional implication. An assumed certificate is not automatically an empirically validated fact. The paid binary benchmark is a restricted theoretical model, not a dataset or experiment. Algorithm 1 exposes initialization, active and padded slots, and the final weight update of equation 3. The proof uses N=R+1N=R+1 scored slots and the outgoing update at r=Rr=R to form WR+1W_R+1. That update creates no extra task or comparator switch. Supplied values of qrq_r and a lawful run protocol are interface inputs, not quantities automatically inferred from native logs. The pseudocode restates the analyzed recursion and does not claim a verified executable implementation of the native controller or generation scheduler. K.6 Reading horizon-dependent conditions correctly In a family of problems all uniform envelopes may depend on T. Uniformity means independent of the comparator at that fixed horizon, not constant as the horizon grows. To read Corollary 8, write these quantities as bT,hresp,T,Nb,T,ST,CT,VT,ηT,ΔTb_T,h_ resp,T,N_b,T,S_T,C_T,V_T, _T, _T. For CT,VT>0C_T,V_T>0, choosing ηT=2CT/(bTVT) _T= 2C_T/(b_TV_T) makes the selection term 2CTbTVT 2C_Tb_TV_T. Zero-capacity cases should use the original inequality, without dividing by zero. For example, conditional on the required certificates, the scaling choices hresp,T=O(1)h_ resp,T=O(1), bT=⌈T1/3⌉b_T= T^1/3 , ST=O(1)S_T=O(1), Nb,T=o(T)N_b,T=o(T), VT=O(T)V_T=O(T), CT=O(log(T+1))C_T=O( (T+1)), and ΔT=o(T) _T=o(T) make each normalized term vanish. The selection term is O(T2/3log(T+1))O(T^2/3 (T+1)). The nominal prefix term is O(T2/3)O(T^2/3) and extra boundaries contribute o(T)o(T). This illustrates the existing corollary, not an assertion that every growing agent supplies these envelopes. In particular, if births force Nb,TN_b,T to be linear, or the native/reference mismatch makes ΔT _T linear, the example does not apply. Table 6: Roles of the results in the conditional native-transfer analysis. Component Role and scope of the contribution Growing selection Classical exponential weights and sharing, checked on history-dependent finite types. Native transfer Directed own-law composition, with application-dependent interface certificates. Local stability Range-sensitive TV telescoping, specialized to actual-path adaptive resource charging. Local generation Conditional coverage and per-task quality bound the generation opportunity gap. Paid benchmark Explicit common-model information lower and primitive upper, near matching only under equation 28. Lean artifact Reproducible verification of the conditional mathematical chain and its explicit interfaces. K.7 Symbols local to the concrete reflection instance Appendix I uses k for the number of generic repair attempts, N for subsequent tasks and reference slots, and T=k+NT=k+N for the full task horizon. This scalar k is not an observation kernel kr(i,o)k_r(i,o). The programs P0,P1,P2P_0,P_1,P_2 are immutable execution identities, not probability laws. The trial bits ζj _j form history HkH_k, and ξ(h)ξ(h) is the all-failed indicator, consistent with the episode failure indicators used in the main generation result. The private bit D concerns the single deployment check. The procedures μ0,μ1 _0, _1 form the own-history class ℳ0M_0. The finite masses wk,s,Qη,hw_k,s,Q_η,h define the coupling Γ in equation 99. The family sets k=n+1k=n+1, N=k2N=k^2, and η=1/kη=1/k. No new global regret definition is introduced. Appendix L Clock alignment and validated mathematical interfaces This appendix makes the interface boundary explicit. An interface is a premise about a specified model, not an unproved conclusion about its regret. The additional proofs below are checked in CompletedClock, CompletedNativeV19, and ObservationBridgeV19. They do not introduce an external controller. L.1 Completed tasks and state-score positions The native score Yt=σt(Ht+1)Y_t= _t(H_t+1) is produced after task t. Take the finite sufficient state St+1S_t+1 to contain the completed history, and write gt(St+1)=Ytg_t(S_t+1)=Y_t. In this appendix gtg_t is the completed-task scorer, not a generation gap. Define the padded state scorer by c~0(S0)=0,c~t+1(St+1)=gt(St+1). c_0(S_0)=0, c_t+1(S_t+1)=g_t(S_t+1). (114) There are T tasks and T+1T+1 scored state positions. A terminal dummy transition after STS_T has zero resource cost and no effect on a scored task. The two processes share a pre-task initial state law, not the law of their first completed score. For a kernel family K, let Wt,nK(s)W^K_t,n(s) be the expected score of the next n completed tasks. Its recursion and its relation to the state-score value are Wt,0K(s) W^K_t,0(s) =0,Wt,n+1K(s)=∑jKt(s,j)[gt(j)+Wt+1,nK(j)], =0, W^K_t,n+1(s)= _jK_t(s,j) [g_t(j)+W^K_t+1,n(j) ], (115) Vt+1,n+1K,c~(s) V^K, c_t+1,n+1(s) =gt(s)+Wt+1,nK(s). =g_t(s)+W^K_t+1,n(s). (116) For n=0n=0, the second identity says that one state position contributes its current score. For the induction step, expand one state transition and apply the same identity at each destination. Nonnegative normalized kernel weights preserve the equality. Expanding the finite trajectory law also proves that W equals the expectation of the sum of completed-task scores. Consequently JTtask(K)=ℙK∑t<Tgt(St+1)=ℙK∑s=0Tc~s(Ss)=JT+1state(K,c~).J_T task(K)=E_P_K _t<Tg_t(S_t+1)=E_P_K _s=0^T c_s(S_s)=J_T+1 state(K, c). (117) The last dummy transition integrates to one. Thus neither the first nor the last task score is removed. The Lean declarations are post_trace_value, shifted_value, and completed_clock. Apply the state-score stability theorem at length T+1T+1 using c~ c. Choose the terminal update identically on both sides, with zero local charge and resource. The actual task budget, generation task count, reference bound UTU_T, and regret normalization remain indexed by T. The resulting completed-task inequality is |JTtask(K)−JTtask(L)|≤H¯ε¯BT/cmin.|J_T task(K)-J_T task(L)|≤ H B_T/c_ . (118) This is CompletedClock.completed_local_gap. With no influence improvement the safe padded local-only bound is (T+1)2ε¯T(T+1)^2 _T. Its normalized sufficient condition is still Tε¯T→0T _T→ 0 as T→∞T→∞. L.2 A validated instance and the exact composition The publication-level CompletedNativeV19.Instance requires unit-range completed-task scores, positive task and run counts, nonnegative resources and activities, zero terminal resources, and integrability of every intermediate expected-score endpoint. The local state contracts use T+1T+1 positions. The reference budget uses T actual tasks. No equality between the two clocks is silently imposed. The remaining reference, episode, and own-law identities are still explicit. For each fixed comparator, the generation theorem gives its budget G=AT+T(δT+fT)G=A_T+T( _T+f_T). Instantiate the reference certificates with this budget and zero inner deployment arrows. Convert the two reference identities using equation 117, invoke the local transfer at the padded state horizon, and convert the two native endpoints back to completed tasks. The reference task bound is unchanged. Thus RT≤UTrest+AT+T(δT+fT)+κ(BA+BC),κ=H¯ε¯/cmin.R_T≤ U_T rest+A_T+T( _T+f_T)+κ(B_A+B_C), κ= H /c_ . (119) The checked endpoint is CompletedNativeV19.Instance.bound. Its variable-domain family theorem invokes this bound before taking limits, using the actual task denominator T. It replaces the unpadded family endpoint as the publication correspondence for Theorem 11. Horizon-dependent model families need not be consistent prefixes of one anytime implementation. No such stronger implementation claim is made. L.3 Connecting local observations to the same experiment law Let h range over finite pre-draw histories, with probabilities a(h)a(h). At each h, a finite observation round has the paper’s accepted-score contract, draw probability php_h, and outcome kernel khk_h. A law witness maps a complete sample ω to its history, draw, and outcome. For every finite test function f it requires Γμf(h,J,O)=∑ha(h)∑iph(i)∑okh(i,o)f(h,i,o).E_ _μf(h,J,O)= _ha(h) _ip_h(i) _ok_h(i,o)f(h,i,o). (120) This specifies the joint law, not merely an identity marginal. Histories can have different finite identity types. Inactive slots can use a singleton absorbing event. For use with the selection recurrence, php_h must be its actual pre-draw probability and the estimator must be its actual update. The comparator coordinate is a function of h, not of the current outcome. Apply the already proved local first-moment identity separately at each h, multiply by a(h)a(h), and sum. Apply the local second-moment inequality in the same way, using a(h)≥0a(h)≥ 0. This gives Γμ[⟨p,ℓ^⟩−ℓ^(v)] _ _μ [ p, - (v) ] =Γμ[ℓref(J)−ℓref(v)], =E_ _μ[ ref(J)- ref(v)], (121) Γμ⟨p,ℓ^2⟩ _ _μ p, ^2 ≤∑ha(h)dh2∑iqh(i)−1. ≤ _ha(h)d_h^2 _iq_h(i)^-1. (122) LawWitness.moment, LawWitness.second, and identified_moment verify these implications and the pointwise pullback identification. The law witness and recurrence identification must be instantiated for a concrete model. There is no claimed automatic constructor from arbitrary native logs to a growing reference execution. The general reference experiment continues to expose these law and moment interfaces. This is the precise boundary of the conditional verification claim. L.4 Accounting is determined by endpoints For three endpoints, a−c=(a−b)+(b−c)a-c=(a-b)+(b-c), checked by adjacent_not_causal. For example, native, reference, and ideal expected losses T,T/2,0T,T/2,0 require both adjacent charges T/2T/2. Both can be consequences of generation failures without being duplicate charges. Only charging the same endpoint difference twice is prohibited. Conversely, an outer full-state charge already includes propagation of its own perturbation, so those same consequences must not be added again to that same arrow. A physical resource may constrain feasibility and affect a task-score difference, but feasibility alone does not add another loss penalty. L.5 Joint feasibility and the scope of sublinearity From TV(Kt,Lt)≤ε¯χtTV(K_t,L_t)≤ _t and cminχt≤rtc_ _t≤ r_t, finite summation gives ∑t<TTV(Kt(St,⋅),Lt(St,⋅))≤ε¯BT/cmin. _t<TTV(K_t(S_t,·),L_t(S_t,·))≤ B_T/c_ . (123) This is accumulated_tv. Also, zero resource implies zero activity and zero local TV, as proved by no_resource_no_error. Thus charging only rare reflection calls cannot cover persistent differences in ordinary selection. Constant-scale discrepancies on a positive fraction of rounds are incompatible with a sublinear resource envelope at fixed ε¯,cmin ,c_ . Coverage attempts, delays and hard budgets must be feasible in the same instance. Corollary 12 supplies a concrete native-transfer witness using direct deployment certificates. The stronger full-state range contracts of the local-resource variant still require their own justification. Corollary 13 derives feasible quotas under quality-dependent coverage and cost contracts. Neither result turns separately desirable exponents into a universal model guarantee. Trial resource use must follow from the same legal design. For the separate sparse benchmark, divide q3T≤mBlogBq^3T≤ mB B by the positive qTqT to obtain q2≤mBlogBqT.q^2≤ mB BqT. (124) The finite inequality is sparse_normalized. It shows why the sparse-family sufficient rate condition requires vanishing observation probabilities. It is not an impossibility result for fixed positive observation probability. The public exogenous registration schedule also does not establish necessity of every endogenous native certificate. Appendix M Related work and research connections Availability and generation. Sleeping bandits address availability (Saha et al., 2020; Nguyen and Mehta, 2024), ballooning models address arriving arms (Ghalme et al., 2020), and growing-expert tracking aggregates expanding pools (Mourtada and Maillard, 2017). Generative action sets use a context-conditioned oracle, permanent reuse, quadratic mismatch and a doubly-optimistic creation-selection controller (Xu et al., 2026). Our Theorem 11 connects causally usable policies to complete native executions through delay, quality and conditional failure. It permits dependent trials. Strongly adaptive regret offers an interval-based perspective (Daniely et al., 2015), while our episodes partition the available-to-aligned endpoint difference. History, feedback, and switching. Classical bandit theory connects specified controllers and observation laws to regret (Lattimore and Szepesvári, 2020; Bubeck and Cesa-Bianchi, 2012). Policy regret (Arora et al., 2012), memory-dependent losses (Anava et al., 2015; Cesa-Bianchi et al., 2013), and Markov games (Nguyen-Tang and Arora, 2025) ground history-responsive comparisons. Our transfer retains the native operation-selection kernel. Theorem 9 bounds full-state discrepancies along actual resource paths. Theorem 11 combines this charge with local generation bounds through ordered score endpoints. Switching-cost bandits (Dekel et al., 2014; Rouyer et al., 2021), feedback-sensitive bounds (Cheng et al., 2023), and feedback graphs (Alon et al., 2015) characterize the role of observation and action-change protocols. Our reference analysis specifies accepted-score calibration and proves the associated observation moments. The supporting model of Theorem 14 uses independent primitive erasures and paid public growth, giving near-matching bounds in the stated sparse regime with common learner, comparator, and cost conventions. Mechanized learning guarantees. Merten et al. (2018) verified multiplicative weights and composed distributed-system guarantees in Coq. Our Lean artifact connects native execution, growing selection, observation, generation, deployment and completed-task clocks. It verifies concrete native instances and a joint quality-budget design. Declaration mappings identify the contracts and endpoints of all thirteen numbered results. Rule-card identities select action kernels, connecting exponential weighting to execution semantics. Full-state stability and conditional failure bounds connect local reflection to total loss. Table 6 summarizes these component roles. Connection to native-agent evaluation. Empirical studies of native LLM online play (Park et al., 2025) motivate analysis of the controller used by the agent. Theorems 9 and 11 connect local generation reliability and full-state deployment stability to the complete native objective. Their joint control determines when the conditional bound is informative. Off-policy evaluation (Dudík et al., 2011) supports analysis of logged decisions. Our reference process additionally requires an identified history law, observation support and accepted-score calibration. Appendix G connects these operational requirements to the transfer interfaces. Appendix N Repeated growth with imperfect validation This second native instance makes validation and subsequent selection genuinely fallible. New context-specific policies are generated in several phases. A false acceptance can overwrite a previously correct native choice and cause errors throughout the remaining phase. The controller follows a recency rule, never runs the reference Bandit, and has no deterministic repair prompt. The construction leaves Theorems 7 and 11 unchanged. It provides a sharper direct calculation and separately verifies compatibility with the existing transfer interfaces. N.1 A frozen generator and an imperfect executable validator Fix integers E,k,m,N≥1E,k,m,N≥ 1 and T=E(k+N)T=E(k+N). There are E public task types, presented in consecutive phases. In phase e, each deployment task has input x=1x=1 and requests output one. Candidate programs are immutable and type-tagged. A correct type-e program returns x on type e and zero on other types. An incorrect candidate returns zero. The initial fallback also returns zero. Correct programs for different types induce different action kernels. Previously registered cards remain in memory, but the legal execution interface calls only current-type cards or the fallback. The same frozen generation kernel, queried with the current type, independently produces a correct or incorrect candidate with probability 1/21/2. No quality label is returned to the controller. A generated handle names immutable content and its version. Each attempt has a fresh handle, even when its behavior duplicates another candidate. Semantic growth across types is distinguished below from the raw number of registrations. The validator tests a candidate on m independent fair inputs in 0,1\0,1\ and accepts only when all outputs match their inputs. A correct current-type program always passes. An incorrect program passes only when every probe is zero. Thus its conditional false-acceptance probability is βm=2−m>0. _m=2^-m>0. (125) This is an imperfect finite-test validator, not a complete program verifier. The sampling protocol is fixed. The native procedure receives candidate handles, test inputs and outputs, and the acceptance decision. It never receives the latent correct/incorrect label. All procedures use the same generation and validation operations. The environment in this instance is deterministic apart from the specified generation and validation randomness. For analysis, a completed attempt has one of three outcomes, denoted 0,1,20,1,2, with probabilities wm(0)=12,wm(1)=βm2,wm(2)=1−βm2.w_m(0)= 12, w_m(1)= _m2, w_m(2)= 1- _m2. (126) Outcome zero is a correct accepted card, one an incorrect accepted card, and two a rejection. These probabilities follow by pushing the fair generation bit and the actual m probe bits through the validator. Outcomes zero and one have the same acceptance signal. The controller can therefore use the acceptance bit without observing this three-way analysis label. N.2 Native execution, retention, and hard resources In each phase, the native learner executes the fallback for the first k tasks and performs one generation attempt after each task. Every accepted candidate is immediately registered and retained. Each acceptance updates a current-type pointer to that newest handle. Rejections preserve the pointer. The following N tasks execute the pointer, or the fallback if none was accepted. The pointer is not repaired during this suffix, even when a task reveals an error. This is an explicit native batching rule, not a claim about every reflective system. Registration does not force immediate deployment. The batch choice pays for its k preparation tasks. The interface still permits other native schedules, including immediate use after a completed registration and a new predictable draw. The construction does not impose a block-boundary restriction on the general model. Generation costs one unit, each probe costs one unit, and each accepted registration costs one unit. Before initiating an attempt, its worst-case cost m+2m+2 is reserved. Generation and probe costs of failed attempts remain charged. Any unused registration reserve is released only after the attempt completes. Every prefix, including an unfinished attempt, then satisfies CA(h)≤∑e<E(m+2)ue(h)≤Ek(m+2)=BT,0≤ue(h)≤k.C_A(h)≤ _e<E(m+2)u_e(h)≤ Ek(m+2)=B_T, 0≤ u_e(h)≤ k. (127) Here ue(h)u_e(h) is the number of initiated attempts in phase e. No registration is possible before initiation. The common prefix cap is BTB_T, available from the start. Stronger time-varying resource schedules would require their own feasibility checks. Resources constrain legal execution and are not added a second time to the task loss. The comparator class ℳM is any nonempty class of complete legal hard-feasible procedures with the same task scorer. For the separation from no reflection, require that it contains the following proactive procedure. At the start of each announced phase, it completes the same k random generation and validation attempts, uses the same latest-accepted rule, and then executes all k+Nk+N tasks. It pays the same worst-case budget and has neither a stronger generator nor a perfect validator. Its observations and memory are generated on its own execution, not copied from the learner. Proposition 16 (Repeated native growth with imperfect validation). The specified native procedure is hard-feasible under equation 127. Let qm,kq_m,k be the probability that its phase pointer is incorrect after k attempts, including the fallback. Then qm,0=1,qm,j+1=βm2+1−βm2qm,j,2−k≤qm,k≤2−k+βm.q_m,0=1, q_m,j+1= _m2+ 1- _m2q_m,j, 2^-k≤ q_m,k≤ 2^-k+ _m. (128) The complete own-law objective satisfies JT(A)=E[k+Nqm,k],RT(A,ℳ)≤E[k+N(2−k+2−m)].J_T(A)=E[k+Nq_m,k], R_T(A,M)≤ E[k+N(2^-k+2^-m)]. (129) The expected number of task types for which a genuinely correct retained policy has been generated is E(1−2−k)E(1-2^-k). If k,m≥2k,m≥ 2 and the proactive comparator belongs to ℳM, the no-reflection procedure has regret at least T/2T/2. With E=k=m→∞E=k=m→∞ and N=k3N=k^3, both positive normalized native regret and normalized hard resources tend to zero. N.3 Proof from the actual execution law Let HjH_j be the completed outcome history in one phase. Its law is recursively generated from equation 126. Let Zj(Hj)∈0,1Z_j(H_j)∈\0,1\ indicate whether the selected pointer is incorrect. Initially Z0=1Z_0=1. An outcome-zero acceptance sets it to zero, an outcome-one acceptance sets it to one, and a rejection retains the old value. Importantly, the control decision in both acceptance cases is identical, namely point to the newest handle. Only analysis of the program output distinguishes the cases. To connect this recursion to executable program content, give attempt j the local handle j and pair it with its phase tag. The registry stores accepted handles without deleting older entries. Induction on j proves that every nonempty pointer names an accepted handle with index less than j. A second induction proves that the correctness of the program at that pointer is exactly 1−Zj1-Z_j. Rejection preserves both the old pointer and the immutable content at its index. Acceptance points to the new content, irrespective of its latent quality. Thus ZjZ_j is the actual program loss at deployment input one, not an independently assigned surrogate score. The same registry induction proves that a correct retained program exists exactly when at least one outcome-zero attempt has occurred. Conditioning on the next outcome Oj+1O_j+1 after the completed prefix gives Oj+1|Hj[Zj+1]=βm2+1−βm2Zj.E_O_j+1 H_j[Z_j+1]= _m2+ 1- _m2Z_j. (130) Integrating this equality yields the recursion in equation 128. This computation derives qm,jq_m,j from the native pointer update rather than assuming a small selection error. For the upper bound, suppose qm,j≤2−j+βmq_m,j≤ 2^-j+ _m. Since 0≤βm≤10≤ _m≤ 1, qm,j+1 q_m,j+1 ≤βm2+1−βm2(2−j+βm) ≤ _m2+ 1- _m2(2^-j+ _m) (131) =2−(j+1)+βm−βm2−(j+1)−βm22≤2−(j+1)+βm. =2^-(j+1)+ _m- _m2^-(j+1)- _m^22≤ 2^-(j+1)+ _m. (132) The initial inequality holds because qm,0=1≤1+βmq_m,0=1≤ 1+ _m. If no correct candidate was generated, the pointer must be incorrect. This event has probability 2−k2^-k, proving the lower bound in equation 128. For every realized phase history, its actual sum of task scores is k+NZk(Hk)k+NZ_k(H_k). Summing over the recursively generated law gives k+Nqm,k+Nq_m,k. The full execution retains old libraries but each current-type kernel ignores their contents, so composing the phase laws gives the first equality in equation 129. Equivalently, linearity of expectation applied to the actual phase rewards gives the same identity. Since every complete comparator has nonnegative common task loss, its own-law expected loss is nonnegative. Subtracting the nonnegative infimum proves the regret upper bound. This argument applies to the original legal comparator class, rather than granting the comparator an unavailable card or a zero-loss oracle. Every generated correct card is accepted and retained. Consequently a type has a correct retained policy exactly when at least one of its k generation bits is correct. The expected number of such types is E(1−2−k)E(1-2^-k). This counts semantically different type-specific policies, not duplicate handles within one type. The expected total number of accepted registrations, including duplicates and incorrect cards, is separately Ek(1+βm)/2Ek(1+ _m)/2. The proactive comparator uses the same random pointer distribution but performs preparation before its tasks. Its own-law objective is JT(μpro)=E(k+N)qm,k=Tqm,k.J_T( _ pro)=E(k+N)q_m,k=Tq_m,k. (133) For k,m≥2k,m≥ 2, the upper bound on qm,kq_m,k is at most 1/21/2. The no-reflection procedure has loss T and therefore regret at least T−JT(μpro)≥T/2T-J_T( _ pro)≥ T/2. This comparator is another noisy reflective procedure with its own generation history, not an omniscient policy. All resource prefixes of both procedures obey the same cap. N.4 Why the validation error is not an instantaneous charge Let MkM_k indicate that no correct card was generated. Define a clean analysis execution that, after the same preparation history, uses a retained correct card if one exists. Then Mk≤ZkM_k≤ Z_k for every history, and Hk[Mk]=2−k,0≤Hk[Zk−Mk]≤βm.E_H_k[M_k]=2^-k, 0 _H_k[Z_k-M_k]≤ _m. (134) The clean execution is not the deployed controller and is not assumed to run a perfect validator. It is an intermediate comparison object. Its advantage over the native pointer is proved from the actual three-outcome law and charged explicitly. For example, a correct acceptance followed by an incorrect acceptance has probability βm/4 _m/4. The correct card remains registered, but the native pointer now calls the incorrect one. In fact, for two attempts the excess error is exactly qm,2−2−2=βm/4>0.q_m,2-2^-2= _m/4>0. (135) Thus an available correct policy does not make the native selection bridge free. A wrong pointer remains active throughout N suffix tasks, so the deployment edge is at most NβmN _m per phase. Counting only βm _m would miss this continuation effect. The growing family below compensates by improving validation as the suffix grows. It does not assume that the global continuation-value range is one. N.5 Connection to the unchanged transfer theorem Condition on a completed phase history before constructing any reference draw. Use the same two-arm reference recursion as Appendix I, with losses one and MkM_k. The second arm represents an actually retained correct card when one exists, and an incorrect fallback otherwise. The clean native suffix has loss NMkNM_k, which is no larger than the reference expected selection loss. The reference initialization, feedback law, code log2 2, and second-moment budget 2N2N are the previously proved ones. The finite controller form of Theorem 7 therefore has the following phase certificates F=k,G=N2−k,EA≤Nβm,EC=DA=DC=Enf=0,F=k, G=N2^-k, E_A≤ N _m, E_C=D_A=D_C=E_ nf=0, (136) with response and switch charges zero inside this phase comparison. The all-correct ideal path has value zero, a valid lower comparison endpoint for any nonnegative own-law comparator value. It is not claimed to be a feasible zero-loss comparator. The direct calculation avoids paying the additional reference selection bound, whereas transfer gives the valid, generally looser inequality RT(A,ℳ)≤E[k+N(2−k+2−m)+log2η+ηN],η>0.R_T(A,M)≤ E [k+N(2^-k+2^-m)+ 2η+η N ], η>0. (137) Each phase uses an independently constructed reference analysis after its preparation has completed. These restarts do not reset the native library. We do not silently invoke a single two-arm fixed-library process across all growing phases. More explicitly, if wm,k(h)w_m,k(h) is the phase history law and Qη,h(g)Q_η,h(g) the actual reference recursion law, define Γ(h,g)=wm,k(h)Qη,h(g) (h,g)=w_m,k(h)Q_η,h(g). Summing over g returns wm,k(h)w_m,k(h), and the native task score does not depend on g. Thus the reference extension preserves the complete native phase marginal. Its phasewise composition preserves the full native execution used above. Comparator objectives retain their respective own laws. This is a causal auxiliary construction, not offline reconstruction from unsupported action logs. The three costs in equation 136 have different endpoints. Preparation losses occur before the suffix. Generation loss is the suffix failure event Mk=1M_k=1. Additional deployment loss is the event Zk=1,Mk=0Z_k=1,M_k=0. These last two events are disjoint. Failed validation and candidate registration consume resources in equation 127, not an additional loss penalty. This prevents charging the same false acceptance as both generation failure and deployment discrepancy. N.6 An explicit family with growing libraries and sublinear resources Take k≥2k≥ 2, m=E=km=E=k and N=k3N=k^3. Then T=k4+k2,BT=k2(k+2),[RT(A,ℳ)]+T≤k−2+21−k,BTT≤k−1+2k−2.T=k^4+k^2, B_T=k^2(k+2), [R_T(A,M)]_+T≤ k^-2+2^1-k, B_TT≤ k^-1+2k^-2. (138) Both right sides tend to zero. The first follows by dividing equation 129 by T≥k4T≥ k^4. The resource calculation uses the same denominator, not a different budget design. The expected number of distinct repaired task types is k(1−2−k)k(1-2^-k), which grows without bound. For the transfer route, choosing η=1/kη=1/k adds at most (log2)k−2+k−1( 2)k^-2+k^-1 to the normalized direct bound, also tending to zero. The guarantee is a horizon-indexed family, not an anytime claim. The restrictions are explicit, including independent template sampling, one-sided validation noise, public type-local phases and no cross-type effect on future generation. The instance supplies repeated semantic growth and persistent imperfect-validation errors within these restrictions. It does not establish joint tightness of the general upper bound or automatic guarantees for arbitrary language-model validators. N.7 Formal correspondence Module ImperfectGrowth connects the native registry and program loss to the probability model through actual_execution. Its actual_regret and actual_no_regret prove the bound and limit, allowing horizon-dependent comparator classes. The full_transfer proof invokes the unchanged transfer through the phase certificates. Appendix H and the declaration mapping cover the intermediate validation, retention and resource proofs. This verifies the specified mathematical program, not deployed language-model code. Reference learning is not necessary for the stronger direct calculation.