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.