The direct observation in [dang2026selecting, Abstract; Sections 3-5 and Tables 1-4] compares 4K, 8K, 12K, and 16K supervision horizons for terminal-agent SFT. In its reported Terminal-Bench v1.0 setting, 12K reaches more tasks than 16K with about thirty percent less training time. The shorter setting under-persisted, the longest setting over-persisted, and the intermediate setting produced the best reported balance. This is a finite terminal-agent observation under one model, teacher corpus, scaffold, and benchmark family; it does not establish a universal horizon, long-term memory, or persistent identity.

The paper's bias-complexity account gives the FTIP hypothesis [dang2026selecting, Sections 5.2 and 6-7; Tables 4-5, 10]. Truncation can increase temporal-supervision bias by removing later decisions, while a longer continuation increases the policy complexity and finite-sample burden. The useful horizon is therefore conditional on the task law, teacher policy, model capacity, verifier, and retained state.

Selective refinement makes the data intervention explicit [dang2026selecting, Sections 6-7; Tables 4-5, 10]. A warm-start model is trained on a shorter horizon, continuation segments are scored by teacher-forced likelihood, and a fixed fraction is retained for longer-horizon refinement. The score measures compatibility with the warm-start policy, not intrinsic truth. High-likelihood selection can improve repeatability; the FTIP protocol tests whether low-likelihood or random selection preserves breadth, rare strategies, and recovery behavior.

A run is premature when it terminates before the declared evidence or recovery condition, productive when it continues through bounded evidence gathering, verification, and recovery, and over-persistent when additional work repeats or explores after task-relevant value has saturated. Record coverage loss separately: a selector can improve repeatability while deleting hard tasks or unusual recovery paths. These terms describe observable behavior; they are not claims about an agent's memory or inner objective.

A long-horizon training trace should preserve the behavior that a later agent must learn: its decisions, evidence, verification, recovery, and the state boundary visible to the continuation. Fix event domains \(\mathcal O_{\rm evt}\), \(\mathcal A_{\rm evt}\), \(\mathcal Y_{\rm evt}\), \(\mathcal E_{\rm evt}\), and \(\mathcal V_{\rm evt}\), together with a termination domain \(\mathcal T_{\rm evt}\) and a boundary domain \(\mathcal S_{\rm boundary}\). The horizon comparison and selective-refinement intervention in [dang2026selecting, Sections 3-7] motivate this adaptation; the typed record below is an FTIP protocol proposal.

For \(H\in \mathbb N\), a trace record is

The components \(o\), \(a\), and \(y\) are observation, action, and outcome events; \(e\) records evidence or an environment-state reference; \(v\) records verification or recovery; \(\tau \) records termination; \(\sigma \) records the state boundary; and \(\kappa \) is token length. The horizon \(H\) and token length \(\kappa \) are separate coordinates. A task may use a declared subtype of each event domain, but it must preserve the coordinate meaning.

The record is a training datum only together with its declared boundary \(\sigma \): a continuation may access exactly the state coordinates allowed by that boundary. The record therefore supports a later selector or run kernel without treating token count as a proxy for the events that make continuation useful.

This is a protocol definition rather than a formal theorem; the event domains and transition semantics must be instantiated by the experiment that uses the record.

Fix a trace record \(T\) from Definition 1.2 and a declared receipt interface with event indicators \(e_{\rm term}(t)\), \(e_{\rm ev}(t)\), \(e_{\rm pass}(t)\), \(e_{\rm fail}(t)\), \(e_{\rm rec}(t)\) and a productive-novelty indicator \(n_{\rm prod}(t)\) for \(0\leq t\leq H\). Let \(u(t)\) be the declared task-value score and \(u^{\rm sat}\) its saturation threshold. The source's reported horizon tradeoff and selective refinement [dang2026selecting, Sections 5.2 and 6-7; Tables 4-5, 10] motivate these observable classes, which are an FTIP proposal. Write

with \(\inf \varnothing :=+\infty \). The receipt declares all indicators and the score as functions of the same run, so the following classes are replayable predicates rather than impressions about an agent's inner state.

A productive trace reaches evidence and a final verifier pass, and any failure before termination is followed by recovery. An over-persistent trace continues after saturation without another declared productive event. The experiment may refine \(n_{\rm prod}\) for a task family, but it must declare that predicate before comparing selectors.

The horizon and selective-refinement observations in [dang2026selecting, Sections 3-7] motivate the following finite classification. Consider a run whose task is to repair a failing build. The retained record contains the failing observation, the source edit, a test execution, and a final verifier pass. With the event interface of Definition 1.3, the test and verification steps contribute to \(e_{\rm ev}\), \(e_{\rm pass}\), and \(n_{\rm prod}\), so the record can satisfy \(\operatorname {Prod}(T)\).

If the test event is removed from the retained record, the same token budget can fail the productive predicate because the evidence chain is incomplete. If identical shell retries continue after \(\tau _{\rm sat}\) with no new productive event, \(\operatorname {Over}(T)\) can hold. This is a finite classification example; it does not claim that every short trace is better or that a model has an inner persistence objective.

The selective-refinement study compares fixed-horizon data interventions under a declared training and evaluation boundary [dang2026selecting, Sections 6-7; Tables 4-5, 10]. A trace-selection experiment is the following finite typed record.

Fix the P0 lifecycle arm set \(\mathcal A\), its boundary map \(r:\mathcal A\to \mathcal J\), mask map \(M:\mathcal A\to \mathcal P(\{s,h,w\})\), and endowment \(E_0\) from § [ftip-00P0] and § [ftip-00OY]. Choose finite nonempty label sets

A split map returns a triple

whose three outputs are pairwise disjoint and satisfy \(|Q_{\rm sel}|>0\), \(|Q_{\rm hold}|>0\); \(Q_{\rm xb}\) may be empty only when the experiment records that no cross-benchmark comparison is made. A randomization map \(\lambda _{\rm pair}:\mathfrak R\to \operatorname {Dist}(\mathcal G\times \mathcal G)\) supplies a joint source law for each paired comparison.

The experiment declares a finite, nonempty arm set \(\mathfrak A\subseteq \mathcal A\times \mathfrak H\times \mathfrak L\times \mathfrak B\times \mathfrak D\times \mathfrak R\). For each \(a\in \mathfrak A\), write its projections as

The arm record additionally supplies one model, teacher, scaffold, verifier, task law, inference protocol, and componentwise budget. These objects are maps of \(a\), not implicit labels; paired arms must agree on every object except the factor named by their comparison. The split attached to \(D_a\) is written \((Q_{\rm sel,a},Q_{\rm hold,a},Q_{\rm xb,a})\); it also supplies a nonempty finite strategy-label set \(\mathfrak S_a\) and a receipt space \(\mathcal R_a^{\rm rec}\) containing a typed held-out outcome \(Y_a\in \mathcal Y_a\cup \{\bot \}\), a declared scalarization \(g_a:\mathcal Y_a\to \mathbb R\), and an admission field. For every paired comparison \((a,a')\), the record additionally declares the finite pairing space \(\mathcal P_{a,a'}:=(Q_{\rm hold,a}\cap Q_{\rm hold,a'}) \times \mathfrak S_a\times \mathfrak S_{a'}\) and a law \(\Lambda _{a,a'}\) on \(\mathcal G\times \mathcal G\times \mathcal P_{a,a'}\). The shared task coordinate in this law is the pairing key; the two strategy coordinates may differ.

For each arm, let \(\mathcal X^{\rm sel}_a\) be the finite candidate-pool space with \(1\leq B_a\leq |\mathcal X^{\rm sel}_a|\), and let \(\mathcal F^{\rm sel}_a\) be the sigma-field generated by the selection-time prefix, teacher-forced score, data-only trace metadata, and \(Q_{\rm sel,a}\). The metadata map excludes held-out outcomes, verifier outcomes, and post-selection continuation events. The selector is a measurable kernel with respect to this sigma-field

It therefore returns a retained index set of the declared size without access to held-out outcomes. Write \(\mathcal I_a:=\{I\subseteq \mathcal X^{\rm sel}_a:|I|=B_a\}\). A run kernel

maps a candidate pool, its retained index set, one component of the paired source draw, a task, and its arm-specific strategy coordinate to a receipt with an event sequence, task and strategy labels, final verifier outcome, typed held-out outcome, admission field, state and artifact hashes, and the charged token, tool, storage, restart, discarded trace, and verification costs, with exactly \(H_a+1\) event slots and a timeout receipt at the final slot when needed. For a paired comparison, \(\Lambda _{a,a'}\) supplies a common held-out task and the two strategy coordinates, while \(\mathcal R_a\) supplies the two source components before the kernels are applied. Thus an arm defines maps and kernels that use the selector output to produce replayable receipts; it does not merely list factors whose later meaning is left implicit.

The reset transition is \(\mathsf {Reset}_{r_a,M_a}\) from § [ftip-00P0]. Horizon, selector, budget, split, and randomization are therefore attached to a concrete P0 state boundary and a concrete run kernel. This is an empirical protocol definition, not a theorem or a claim that any selector improves behavior.

The source compares retained-horizon choices under declared task and evaluation boundaries [dang2026selecting, Sections 6-7; Tables 4-5, 10]. Fix an arm \(a\in \mathfrak A\) from Definition 2.1 and a positive run count \(N_a\). Each receipt \(R_{a,i}\) exposes a finite event sequence \((e^{\rm term},e^{\rm ev},e^{\rm pass},e^{\rm fail},e^{\rm rec}, n^{\rm prod})_{t=0}^{H_a}\), a task label \(q_{a,i}\), a strategy label \(s_{a,i}\), a measurable task-value score \(u_{a,i}(t)\), a declared saturation threshold \(u_a^{\rm sat}\), and a typed held-out outcome \(Y_{a,i}\in \mathcal Y_a\cup \{\bot \}\), final verifier outcome \(v_{a,i}\), and complete-admission indicator \(A_{a,i}\). Define \(A_{a,i}:=\mathbf 1[q_{a,i}\in Q_{\rm hold,a}\land v_{a,i}=1 \land Y_{a,i}\in \mathcal Y_a]\); when \(A_{a,i}=0\), set \(Y_{a,i}:=\bot \). The receipt contract emits a terminal event by \(H_a\); an execution that would not terminate naturally receives a timeout terminal event at \(H_a\) and \(A_{a,i}=0\). Put \(\overline {\mathbb N}:=\mathbb N\cup \{+\infty \}\) and \(\inf \varnothing :=+\infty \).

Define the receipt predicates

Here \(n^{\rm prod}_{a,i}(t)\) is a declared productive-novelty indicator in the receipt, and \(I^{\rm rec}\) is zero when no failure precedes recovery. The five run rates are functions of the receipts, with the declared denominator \(N_a\):

For the finite held-out set, task and strategy coverage are

where \(\mathfrak S_a\) is a declared nonempty strategy-label set. Every receipt reports both positive denominators and the admission rule.

For two paired arms \(a\) and \(a'\) that differ in one declared factor, let \(N:=\min (N_a,N_{a'})\). Define the common admitted index set \(J_{a,a'}:=\{i\leq N:A_{a,i}=A_{a',i}=1\}\) and \(N_{\rm pair}:=|J_{a,a'}|\). For \(i\in J_{a,a'}\), let \(Y_{a,i}\) and \(Y_{a',i}\) be their admitted held-out outcomes under the shared pairing law \(\Lambda _{a,a'}\), so \(q_{a,i}=q_{a',i}\). Compare their declared scalarizations \(g_a(Y_{a,i})\) and \(g_{a'}(Y_{a',i})\). When \(N_{\rm pair}\geq 2\), the primary finite contrast and its paired sample variance are

When \(N_{\rm pair}=1\), report the single paired contrast but set \(\widehat V_{a,a'}:=\bot \); when \(N_{\rm pair}=0\), the paired contrast is undefined and the missingness is reported. These are finite estimators under the declared arm, split, admission rule, and coupling; they are not a universal selector law.

The selective-refinement comparison motivates contrasting repeatability and coverage under a fixed retained budget [dang2026selecting, Sections 6-7; Tables 4-5, 10]. Consider two arms from Definition 2.1 with the same P0 boundary, model, task split, verifier, budget, and paired assignment law. They differ only in the selector: \(a\) retains the highest teacher-forced scores and \(a'\) retains a coverage-stratified subset. Both have \(Q_{\rm hold}=\{q_1,q_2\}\) and \(\mathfrak S=\{s_1,s_2\}\). The paired assignment law gives the same held-out task at indices 1 and 2; arm \(a'\) has one additional admitted coverage run at index 3. Take \(g_a=g_{a'}=\operatorname {id}_{\{0,1\}}\). The receipts are

The first two rows are the common paired indices, so \(N_a=2\), \(N_{a'}=3\), and \(N_{\rm pair}=2\). Both arms have \(\widehat p^{\rm prod}=1\); the third row is included in arm \(a'\)'s coverage and run-rate denominators but not in the paired contrast. Thus \(\widehat C^{\rm task}_a=\widehat C^{\rm strat}_a=\tfrac 12\) and \(\widehat C^{\rm task}_{a'}=\widehat C^{\rm strat}_{a'}=1\), while \(\widehat \Delta _{a,a'}=-\tfrac 12\). The calculation shows why a repeatability rate alone cannot identify coverage: the two selectors have the same productive rate but different admitted task and strategy support. This is a finite FTIP construction using the typed receipt and pairing definitions, not a source result.