Sampling and replay protocol [ftip-00OW]

✍️sourceAGENTDRAFTED

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

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

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

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

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:

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.