Each result concerns its declared carriers \(X_1,\ldots ,X_n\), with fixed equality and order conventions. Finiteness, probability laws, and positivity conditions are hypotheses of the result; they cannot be inferred from a finite observation alone.

For \(B\in \mathbb N\) independent discovery events with the probabilities declared in Convention [ftip-0077], the identity in Theorem [ftip-0078] gives \(\Pr (D_B)=1-\prod _{i=1}^{B}(1-p_i)\).

Under \(0<p<1\), \(0<\delta <1\), and an integer budget \(B\geq 1\), the failure constraint is equivalent to the following bound.

The result is proved in Corollary [ftip-0079].

Under the finite-carrier and positive-temperature hypotheses of Theorem [ftip-007C], normalized exponential tilting preserves the base law's positive support.

For a finite common feasible set and a common regularizer, the uniform proxy error hypothesis in Definition [ftip-007G] yields the two-epsilon objective regret bound proved in Theorem [ftip-007H]; the conclusion concerns the regularized objective named there.

If the evaluation laws and finite response space satisfy the total-variation hypotheses of Theorem [ftip-00GM], then the expectation difference is bounded by the stated sup-norm times total variation.

For finite response set \(\mathcal Y\) and deterministic rewards, a reward channel that refines the equality partition of another channel separates at least as many response classes, as proved in Lemma [ftip-00AG].

If the execution map is deterministic in all coordinates fixed by Definition [ftip-00HF], then equal input, revision, environment, and seed records produce equal finite traces, as proved in Theorem [ftip-00HG].

For the finite transcript and world kernels declared in Definition [ftip-008C]--Definition [ftip-008D], observationally equivalent worlds induce the same output law for any common randomized post-training kernel, as proved in Theorem [ftip-007S].

Under the typed audit record of Definition [ftip-00HL], a commit is admissible exactly when all required checks pass, the digest matches, and the recorded decision is \(commit\), as proved in Theorem [ftip-00HM].

A finite audit plan with nonnegative stage costs is admissible exactly when its declared additive cost is within budget; adding a positive stage beyond slack is inadmissible, by Theorem [ftip-00HX].

A finite assignment satisfying a claim's hypotheses and violating its conclusion disproves that universal claim. It does not estimate how often the failure occurs under another distribution or establish a general failure rate.

A conclusion about fixed carriers, policies, feedback, budgets, and evaluation laws need not survive a change to those objects. Finite zero hits do not imply zero support, empirical benchmark movement does not imply acquisition, and an exact-optimizer result need not hold for an approximate optimizer without an additional error bound.

The two-task examples in Example [ftip-007E] and Example [ftip-00A3] show that equal one-shot averages or zero observed hits can coexist with different coverage or nonzero latent rates. These conclusions use their declared iid model and do not estimate rates outside it.

In the two-point construction of Example [ftip-007J], training-law average error is small while evaluation selection reverses. The missing hypothesis is a uniform bound on the evaluated feasible set; an informal promise of similar distributions does not supply it.

For DGG, the untied head identity and its finite-batch Jensen bound in Theorem [ftip-007Z] and Theorem [ftip-0081] differ from an intermediate-occurrence bound. A shared intermediate weight requires the sum over all occurrences in Theorem [ftip-007Z]; the source's local hypotheses do not establish its claimed total-gradient bound in [miao2026when, Section 4.2.1, Lemma 1, Theorem 1, and Appendix A.3]. The cancellation example Example [ftip-0084] also separates the active clipping interval from the raw-surrogate extension.

NExt's empirical checkpoint forecasts in [chen2026lowrank, Sections 3.2, 4.1--4.3, and 5.1] do not establish a universal subspace-collapse, capability, or speed theorem. The spectral and evaluation quantities in Definition [ftip-0086] through Remark [ftip-008B] measure different trajectory properties.

Use \(\mathcal X\) for prompts, \(\mathcal Y\) for finite responses, \(\Omega \) for sample space, \(\mathsf P\) for a declared protocol, and \(\mu \) for a prompt law. A probability law is written \(\Pr \) only after its sample space is named.

Use \(\pi \) for a policy, \(\pi _{\rm base}\) for a reference policy, and \(\pi _\theta \) for a parameterized policy. A policy is always typed as a kernel from the declared prompt carrier to the declared response carrier.

Use \(r:\mathcal X\times \mathcal Y\to \mathbb R\) for a deterministic reward and \(u\) for an evaluation utility. Proxy, verifier, and process rewards retain their local subscripts; no bare symbol silently changes meaning.

Use \(M\) for a model artifact, \(\mathsf E\) for an evaluation protocol, and \(J_{\mathsf E}(M)\) for its declared score. A comparison must state the invariant evaluation law before subtracting two scores.

Use \(z_{0:n}\) for a finite trace, \(s_t\) for a harness state, \(\ell \) for a lineage, and \(c\) for an execution cost. Event logs and summaries are distinct carriers even when one is computed from the other.