Prompt and research-state transport [ftip-00G8]
✍️source

    Definition 1. Research-state observable [ftip-00G9]

      For a finite record space \(\mathcal R\), an observable is a map \(h:\mathcal R\to \mathcal H\). A summary-only evaluator sees \(h(r)\) and not the underlying record \(r\); the omitted coordinates are unavailable to that evaluator.

      Definition 2. Compaction kernel [ftip-00GA]

        A compaction kernel is a randomized map \(K(dh\mid r)\) from records in \(\mathcal R\) to summaries in \(\mathcal H\). A deterministic summary is the special case \(K(dh\mid r)=\delta _{h(r)}\).

        Theorem 3. Summary-only indistinguishability [ftip-00GB]

          Let \(r,r'\in \mathcal R\) induce the same summary law under the kernel in Definition 2. Any randomized decision rule that receives only that summary has the same output law in the two worlds.

          Proof. 

            The output law is the pushforward of the common summary law through the same decision kernel. Pushforwards of equal finite measures are equal.

            Example 4. An omitted feasibility constraint [ftip-00GC]

              Two research records can share every summary score while one contains a withdrawn lemma and the other contains a feasible proof plan. A summary-only selector therefore chooses identically, although the correct next action differs. This is a finite witness to information loss, not a claim about a particular model.

              Remark 5. Long-horizon records are empirical transport evidence [ftip-00GD]

                The case study in [li2026longhorizon], Sections 4--7, reports file-based memory, human steering, and research-state failures under one system and task. It motivates explicit observables and omitted constraints; it does not supply the finite theorem in Theorem 3 or a general model capability law.

                References

                  Reference. Long-Horizon AI Research for Grothendieck Constant: A Case Study in Human--AI Mathematical Collaboration [li2026longhorizon]

                  @article{li2026longhorizon,
  title = {Long-Horizon AI Research for Grothendieck Constant: A Case Study in Human--AI Mathematical Collaboration},
  author = {Li, Alan and Saha, Rahul and Xue, Anton and Chaudhuri, Swarat and Klivans, Adam and Kothari, Pravesh K. and Meka, Raghu},
  year = {2026},
  url = {https://arxiv.org/abs/2608.11195v1},
  journal = {arXiv preprint arXiv:2608.11195}
}

                  Context

                    Evaluation transport and matched protocols [ftip-00F9]

                      This section compares post-training artifacts only through declared evaluation laws, inference protocols, utilities, seeds, and budgets. It proves finite transport statements locally and treats long-horizon research-state records as empirical evidence, not as theorems.

                      Evaluation laws and couplings [ftip-00FA]

                        Convention. A named evaluation experiment [ftip-00FB]

                          A named evaluation experiment records the artifact, task law, inference protocol, evaluator, seed kernel, budget, and sampling unit. Two reported scores are comparable only after these coordinates and their intended target have been stated.

                          Definition. Evaluation law [ftip-00FC]

                            For a fixed evaluation interface from Convention [ftip-005D], an evaluation law is a probability measure \(\mathsf Q\) on the finite outcome space \(\mathcal Z=\mathcal X_{\mathsf T_{\rm ev}}\times \mathcal O_{\mathsf T_{\rm ev}}\) with random pair \((X,O)\sim \mathsf Q\). Its score for artifact \(M\) is a bounded measurable map \(s_M:\mathcal Z\to [0,1]\). Write \(J_{\mathsf Q}(M)=\mathbb E_{\mathsf Q}[s_M(X,O)]\).

                            Definition. Matched evaluation pair [ftip-00FD]

                              A matched evaluation pair is \((\mathsf Q,\mathsf I,b,\Lambda )\) and \((\mathsf Q',\mathsf I',b',\Lambda ')\) together with a coupling \((Z,Z')\) whose marginals are the two laws. The pair is matched on the declared coordinates when the task, utility, evaluator version, and sampling unit are shared; any changed coordinate is named.

                              Definition. Paired finite score estimator [ftip-00FE]

                                For iid coupled draws \((Z_j,Z'_j)_{j=1}^m\), define \(\widehat \Delta _m=m^{-1}\sum _{j=1}^m(s_M(Z_j)-s_{M'}(Z'_j))\). The pairing is part of the estimator specification; it does not silently identify the two evaluation laws.

                                Theorem. Unbiasedness of the paired score estimator [ftip-00FF]

                                  Under the iid coupling in Definition [ftip-00FE], \(\mathbb E[\widehat \Delta _m]=J_{\mathsf Q}(M)-J_{\mathsf Q'}(M')\).

                                  Proof. 

                                    Linearity of expectation gives the displayed identity.

                                    \[ \mathbb E[\widehat \Delta _m] =m^{-1}\sum _j\left (\mathbb E[s_M(Z_j)]- \mathbb E[s_{M'}(Z'_j)]\right ). \]

                                    The coupling fixes the joint sampling but does not change either marginal, so the two terms are the stated expectations.

                                    Example. Common seeds can reduce paired variance [ftip-00G0]

                                      If \(s_M(Z)=s_{M'}(Z')\) almost surely under a common-seed coupling, then \(\widehat \Delta _m=0\) for every sample even when independent sampling would have nonzero variance. This is a variance statement, not evidence that the two artifacts have equal behavior on a different law.

                                      Remark. A coupling does not merge estimands [ftip-00G1]

                                        The result in Theorem [ftip-00FF] follows from its displayed hypotheses. A shared seed can make a paired comparison precise while the changed task law, evaluator, or inference budget still changes the estimand. No causal effect follows without a declared intervention and matched coordinates.

                                        Utility transport [ftip-00G2]

                                          Definition. Bounded utility perturbation [ftip-00G3]

                                            On a common finite outcome law \(\mathsf Q\), let each artifact \(M\) have score maps \(s_M,t_M:\mathcal Z\to [0,1]\). They have perturbation radius \(\varepsilon =\sup _{M,\,z\in \operatorname {supp}(\mathsf Q)} |s_M(z)-t_M(z)|\) when \(0\leq \varepsilon \leq 1\); write \(J_s(M)=\mathbb E_{\mathsf Q}[s_M]\) and \(J_t(M)=\mathbb E_{\mathsf Q}[t_M]\).

                                            Theorem. Direct utility transport bound [ftip-00G4]

                                              Under Definition [ftip-00G3], every artifact \(M\) satisfies \(|J_s(M)-J_t(M)|\leq \varepsilon \).

                                              Proof. 

                                                Pointwise bounds give \(-\varepsilon \leq s_M(z)-t_M(z)\leq \varepsilon \). Taking expectations preserves both inequalities.

                                                Corollary. Transporting an artifact comparison [ftip-00G5]

                                                  If two artifacts \(M_1,M_0\) are scored by both \(s\) and \(t\) under the same law and \(\lVert s-t\rVert _{\infty ,\mathsf Q}\leq \varepsilon \), then the gain difference obeys \(|(J_s(M_1)-J_s(M_0))-(J_t(M_1)-J_t(M_0))| \leq 2\varepsilon \). This is a finite utility perturbation bound, not a training or distribution-shift theorem.

                                                  Example. Equal aggregate score can hide a slice reversal [ftip-00G6]

                                                    On equally likely outcomes \(a,b\), take score vectors \((s_{M_1}(a),s_{M_1}(b))=(1,0)\) and \((s_{M_0}(a),s_{M_0}(b))=(0,1)\); a second score map swaps coordinates. Both artifacts have aggregate score \(1/2\) under both maps, but their per-outcome ordering reverses. Aggregate transport alone does not identify localized behavior.

                                                    Remark. Common domains are a transport hypothesis [ftip-00G7]

                                                      The bound in Theorem [ftip-00G4] requires the same finite outcome support. Changing prompts, parsers, evaluators, or inference budgets is a new law and must be recorded rather than hidden inside a score perturbation.

                                                      Prompt and research-state transport [ftip-00G8]
                                                      ✍️source

                                                        Definition. Research-state observable [ftip-00G9]

                                                          For a finite record space \(\mathcal R\), an observable is a map \(h:\mathcal R\to \mathcal H\). A summary-only evaluator sees \(h(r)\) and not the underlying record \(r\); the omitted coordinates are unavailable to that evaluator.

                                                          Definition. Compaction kernel [ftip-00GA]

                                                            A compaction kernel is a randomized map \(K(dh\mid r)\) from records in \(\mathcal R\) to summaries in \(\mathcal H\). A deterministic summary is the special case \(K(dh\mid r)=\delta _{h(r)}\).

                                                            Theorem. Summary-only indistinguishability [ftip-00GB]

                                                              Let \(r,r'\in \mathcal R\) induce the same summary law under the kernel in Definition [ftip-00GA]. Any randomized decision rule that receives only that summary has the same output law in the two worlds.

                                                              Proof. 

                                                                The output law is the pushforward of the common summary law through the same decision kernel. Pushforwards of equal finite measures are equal.

                                                                Example. An omitted feasibility constraint [ftip-00GC]

                                                                  Two research records can share every summary score while one contains a withdrawn lemma and the other contains a feasible proof plan. A summary-only selector therefore chooses identically, although the correct next action differs. This is a finite witness to information loss, not a claim about a particular model.

                                                                  Remark. Long-horizon records are empirical transport evidence [ftip-00GD]

                                                                    The case study in [li2026longhorizon], Sections 4--7, reports file-based memory, human steering, and research-state failures under one system and task. It motivates explicit observables and omitted constraints; it does not supply the finite theorem in Theorem [ftip-00GB] or a general model capability law.

                                                                    Evaluation cells and budget accounting [ftip-00GE]

                                                                      Definition. Evaluation cell [ftip-00GF]

                                                                        An evaluation cell is \(C=(M,\mathsf Q,\mathsf I,b,\Lambda ,v)\), where \(M\) is an artifact, \(\mathsf Q\) a task law, \(\mathsf I\) an inference protocol, \(b\) a budget, \(\Lambda \) a seed kernel, and \(v\) an evaluator version. A cell comparison may differ in named coordinates only.

                                                                        Lemma. Additive evaluation cost [ftip-00GG]

                                                                          For a finite evaluation plan with disjoint stages of costs \(c_1,\ldots ,c_k\in \mathbb R_{\geq 0}\), total cost is \(c=\sum _{i=1}^k c_i\). Appending a stage increases cost by its declared amount and cannot preserve a budget \(B\) unless the remaining slack covers it.

                                                                          Proof. 

                                                                            The statement is the associativity and monotonicity of finite sums.

                                                                            Theorem. Budget-preserving matched comparison [ftip-00GH]

                                                                              Let two evaluation plans use the same declared stages except for a substitution whose cost is at most the replaced stage cost. If their common prefix cost is \(c_0\) and both suffix costs fit \(B-c_0\), then both cells in Definition [ftip-00GF] are admissible under budget \(B\).

                                                                              Proof. 

                                                                                Apply Lemma [ftip-00GG] to the common prefix and each suffix. The assumed inequalities give total cost at most \(B\) in each plan.

                                                                                Example. Cost-balanced evaluation cells [ftip-00GI]

                                                                                  A paired run can spend \(B=100\) units as 40 units of inference, 20 of evaluator calls, and 40 of audit. Replacing 10 inference units by 10 audit units preserves the budget, but changes the cell and must not be described as the same inference protocol.

                                                                                  Remark. Execution and evaluator confounds [ftip-00GJ]

                                                                                    A score change can arise from the artifact, prompt law, inference budget, parser, evaluator version, or execution failure. A matched-cell report names these coordinates before interpreting a paired gain.

                                                                                    Distribution shift and ranking reversals [ftip-00GK]

                                                                                      Example. Train and evaluation laws can reverse a ranking [ftip-00GL]

                                                                                        Let \(\mathsf Q_{\rm tr}\) put masses \(.9,.1\) on \(a,b\), and let \(\mathsf Q_{\rm ev}\) swap them. Artifacts \(M_1,M_0\) with score vectors \((s_{M_1}(a),s_{M_1}(b))=(1,0)\) and \((s_{M_0}(a),s_{M_0}(b))=(0,1)\) rank oppositely under the two laws. A training score is not an evaluation transport certificate.

                                                                                        Theorem. Total-variation transport bound [ftip-00GM]

                                                                                          For any score \(s:\mathcal Z\to [0,1]\) and finite laws \(\mathsf Q,\mathsf Q'\), \(|\mathbb E_{\mathsf Q}s-\mathbb E_{\mathsf Q'}s|\leq \lVert \mathsf Q-\mathsf Q'\rVert _{\rm TV}\), where \(\lVert \mathsf Q-\mathsf Q'\rVert _{\rm TV}:=\frac 12\sum _{z\in \mathcal Z} |\mathsf Q(z)-\mathsf Q'(z)|\).

                                                                                          Proof. 

                                                                                            Expand the finite expectation difference and use \(|s(z)|\leq 1\). The positive and negative parts are bounded by the total variation mass, giving the displayed inequality.

                                                                                            Example. A sharp two-point transport bound [ftip-00GN]

                                                                                              On \(\mathcal Z=\{a,b\}\), let \(s(a)=1,s(b)=0\), and let \(\mathsf Q(a)=1\), \(\mathsf Q'(a)=1-\eta \), and \(\mathsf Q'(b)=\eta \). The score difference and total variation distance are both \(\eta \).

                                                                                              Remark. What transport does not identify [ftip-00GO]

                                                                                                The bounds above transport a declared score across a declared law. They do not identify why an artifact changed, establish support expansion, prove generalization, or order different evaluators whose outcome spaces differ.

                                                                                                Example. A minimal evaluation trace [ftip-00GP]

                                                                                                  A reproducible record is \((M,\mathsf Q,\mathsf I,b,\Lambda ,v,m, \widehat \Delta _m,c)\), listing the cells, sample count, paired estimate, and cost. Replaying this tuple reproduces the estimator target only when the recorded laws and versions remain available.

                                                                                                  Remark. Execution controls for a matched evaluation [ftip-00GQ]

                                                                                                    A matched evaluation requires execution gates, contamination checks, grader calibration, and an audit of the result before it is committed. These controls make the comparison auditable; they do not by themselves establish capability acquisition.

                                                                                                    Sampling claims become comparable only when the task law, action serializer, verifier, and replay certificate are fixed together; § [ftip-00OW] gives that boundary.

                                                                                                    Sampling and replay protocol [ftip-00OW]

                                                                                                      A sampling comparison begins with a task interface and an evaluation inference protocol. Fix the task law from Notation [ftip-001N], the inference budget, the model artifact, the prompt and tokenizer, and the serializer \(S\) that maps a public history to a token or tool action. Let an intervention \(I\) change only the named sampler, random source, harness state, or evaluator coordinate; every other coordinate is held fixed. The four readouts below keep distribution fit, action behavior, verification, and replay evidence distinct.

                                                                                                      Protocol estimands. For a declared finite output set \(\mathcal Y\), target law \(P^*\in \mathsf {Prob}(\mathcal Y)\), sample size \(n\geq 1\), and realized outputs \(Y_1,\ldots ,Y_n\in \mathcal Y\), define the target-distribution fit readout by

                                                                                                      \[ \widehat P_{I,n}(y)=\frac 1n\sum _{j=1}^{n}{\bf 1}\{Y_j=y\},\qquad E_{\rm dist}(I)=d(\widehat P_{I,n},P^*), \]

                                                                                                      where \(d\) is a declared divergence or goodness-of-fit functional on \(\mathsf {Prob}(\mathcal Y)\). The task law, output serializer, sample size and random-source law are part of the intervention record; logits alone do not determine this readout.

                                                                                                      For horizon \(T\geq 1\), public histories \(H_t\in \mathcal H_t\), and serialized actions \(A_t\in \mathcal A_t\), the action-law readout is the empirical measure

                                                                                                      \[ \widehat \Pi _{I,n}=\frac 1n\sum _{j=1}^{n}\delta _{(H_{j,0},A_{j,0},\ldots ,H_{j,T-1},A_{j,T-1})}. \]

                                                                                                      The non-anticipating policy contract in Definition [ftip-0023] supplies the admissible action kernels and requires the serializer to be declared. Thus \(\widehat \Pi _{I,n}\) records what the system did on the declared histories; it does not establish that those actions follow \(P^*\).

                                                                                                      For the evaluation utility and joint evaluation law \(\nu _I\) induced by the fixed task law, protocol randomness, inference seed, and evaluator seed, define the verifier readout by

                                                                                                      \[ E_{\rm ver}(I)=\int u_{\mathsf T}(x,o;\omega )\,d\nu _I(x,o,\omega ). \]

                                                                                                      A binary verifier is the special case of the indicator in Definition [ftip-0046]; its version and evidence record follow Definition [ftip-0047]. The expectation is taken only when the measurability and integrability conditions of Definition [ftip-001T] and Convention [ftip-005D] hold. A successful check does not identify which sampler or harness state produced its trajectory.

                                                                                                      Replay is evidence rather than a fourth scalar estimand. A replay certificate is the tuple

                                                                                                      \[ \mathcal R_I=(M,x,S,Q_I,\nu _I,\rho _I,h_0,L_n,\boldsymbol v,(F_v)_v,\nu _{\rm pol},e_{\rm ver},C(I)), \]

                                                                                                      where \(\rho _I\) is the realized random-source state and \(L_n\) is the persistent event stream, \(h_0\), \(\boldsymbol v\) and \(F_v\) give the materialized harness state, \(\nu _{\rm pol}\) is the content-addressed policy stamp from Definition [ftip-004Z], \(e_{\rm ver}\) is verifier evidence from Definition [ftip-0047], and \(C(I)\) is the lifecycle cost vector. Equality of all these fields, including the task instance, model, sampler, serializer and policy stamp carried by the certificate or its event record, is the replay identity. The theorem in Theorem [ftip-00C9] then gives equal materialized state; replay identity still does not imply correctness, as Example [ftip-00HH] records.

                                                                                                      Protocol proposal. The transition boundary is typed by the following finite sequence. The protocol computes logits from the model, task input and current public history; the sampler \(Q_I\) consumes those logits and random source \(\rho _I\) to produce \(A_t\); the event constructor records \(e_t=\operatorname {event}(H_t,A_t)\) and the public-history observer records \(H_{t+1}=\operatorname {observe}(H_t,e_t)\); the harness appends the same event and folds it:

                                                                                                      \[ L_{t+1}=\operatorname {append}(L_t,e_t),\qquad H_{t+1}=\operatorname {observe}(H_t,e_t),\qquad h_{t+1}=F_{v_t}(h_t,e_t),\qquad (o,c)=\mathsf I(M,x,b;\xi ). \]

                                                                                                      The evaluator consumes the completed outcome and its evidence, not the pre-verification token. An intervention must name the changed member of \((M,x,S,Q_I,\rho _I,h_0,\boldsymbol v,e_{\rm ver})\) and the held-fixed members. A state update, retry, or evaluator call is a new event and contributes to the recorded lifecycle cost vector; these are not silently absorbed into the model effect.

                                                                                                      Source observation. Gu et al. (arXiv:2604.06543v2, PDF pp. 4-10) find biased direct sampling and reliable seed-to-distribution transformations in the tested models ([gu2026stochasticity, Sections 3, 5, and 6]). H1 reports a simple Lean loop whose interface, verifier feedback, and self-reflection support a formal-Lean comparison (submitted 30 September 2026, PDF pp. 2-3 and 8-11; [moalla2026h1, Sections 2.1-2.2 and 4]); its reported benchmark results use additional empirical sections ([moalla2026h1, Sections 3.1-3.3]). Stateless Language Agents assign persistent experiment state to the harness while Advisor and Worker calls are stateless (arXiv:2610.07625v1, PDF pp. 3-12; [zhang2026statelessagents, Sections 2.2, 3.1-3.2, and 4.2-4.3]).

                                                                                                      FTIP deduction. These observations justify separating the model, serializer, sampler, random source, harness, verifier, and lifecycle ledger. The empirical protocol itself has no corresponding Lean declaration in the searched Forest, formal-math, TauCetiReview, or TauCetiWorker revisions; Theorem [ftip-00C9] supports only the deterministic event-folding sub-result.

                                                                                                      Finite replay check. Take \(\mathcal A_0=\{0,1\}\), horizon \(T=2\), \(h_0=()\), and events \(e_0=\operatorname {call}(0)\) and \(e_1=\operatorname {verify}(1)\). Let \(F(h,e)=h\mathbin {\|}e\) and \(L_2=(e_0,e_1)\). Two runs with the same policy stamp, realized random-source state, verifier identity, event version, fold map and cost vector have the same \(\mathcal R_I\); the recursion in Theorem [ftip-00C9] checks \(h_2=((\operatorname {call}(0)), (\operatorname {verify}(1)))\). Changing the recorded random-source state therefore fails the replay-identity check, even if a coincidentally identical event stream is produced. This finite certificate is the Phase A boundary: it makes replay auditable without claiming a universal stochasticity law.