Finite probability and execution results [ftip-00I2]
✍️source

    The conclusions depend on their declared probability laws, finite index sets, positivity conditions, and execution inputs. Changing one of these assumptions can change the result even when the observed score is unchanged.

    Convention 1. Domains of the finite results [ftip-00I5]

      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.

      Theorem 2. Independent discovery probability [ftip-00I7]

        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)\).

        Theorem 3. Discovery budget for a failure threshold [ftip-00I8]

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

          \[B\geq \left \lceil \frac {\log \delta }{\log (1-p)}\right \rceil .\]

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

          Theorem 4. Support under finite exponential tilting [ftip-00I9]

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

            Theorem 5. Uniform proxy error and objective regret [ftip-00IA]

              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.

              Theorem 6. Utility under a change of evaluation law [ftip-00IB]

                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.

                Theorem 7. Response classes under feedback refinement [ftip-00IC]

                  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].

                  Theorem 8. Equal execution inputs give equal replay traces [ftip-00IJ]

                    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].

                    Theorem 9. Observational equivalence under a common update kernel [ftip-00IK]

                      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].

                      Theorem 10. Conditions for an admissible commit decision [ftip-00IL]

                        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].

                        Theorem 11. Admission of a finite audit plan [ftip-00IM]

                          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].

                          Context

                            Probability, information, and execution [ftip-00I1]

                              Discovery probabilities, support, proxy error, feedback resolution, and replay each constrain a different part of a comparison. Capability remains conditional behavior under a declared intervention and evaluation law, rather than a scalar latent property.

                              Finite probability and execution results [ftip-00I2]
                              ✍️source

                                The conclusions depend on their declared probability laws, finite index sets, positivity conditions, and execution inputs. Changing one of these assumptions can change the result even when the observed score is unchanged.

                                Convention. Domains of the finite results [ftip-00I5]

                                  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.

                                  Theorem. Independent discovery probability [ftip-00I7]

                                    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)\).

                                    Theorem. Discovery budget for a failure threshold [ftip-00I8]

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

                                      \[B\geq \left \lceil \frac {\log \delta }{\log (1-p)}\right \rceil .\]

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

                                      Theorem. Support under finite exponential tilting [ftip-00I9]

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

                                        Theorem. Uniform proxy error and objective regret [ftip-00IA]

                                          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.

                                          Theorem. Utility under a change of evaluation law [ftip-00IB]

                                            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.

                                            Theorem. Response classes under feedback refinement [ftip-00IC]

                                              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].

                                              Theorem. Equal execution inputs give equal replay traces [ftip-00IJ]

                                                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].

                                                Theorem. Observational equivalence under a common update kernel [ftip-00IK]

                                                  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].

                                                  Theorem. Conditions for an admissible commit decision [ftip-00IL]

                                                    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].

                                                    Theorem. Admission of a finite audit plan [ftip-00IM]

                                                      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].

                                                      Counterexamples and restricted assumptions [ftip-00ID]

                                                        Finite constructions can separate average success from coverage, proxy accuracy from evaluation quality, and observed gradients from the hypotheses needed to bound them. Each separation identifies an assumption that a stronger conclusion would require.

                                                        Remark. What a finite counterexample establishes [ftip-00IE]

                                                          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.

                                                          Remark. Changing the model or evaluation changes the claim [ftip-00IF]

                                                            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.

                                                            Example. Equal averages and zero hits do not identify coverage [ftip-00IG]

                                                              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.

                                                              Example. Small training-law error can reverse evaluation selection [ftip-00IH]

                                                                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.

                                                                Remark. Untied heads, shared gradients, and checkpoint forecasts [ftip-00II]

                                                                  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.

                                                                  Mathematical notation [ftip-00IN]

                                                                    Prompt and response spaces, probability laws, policies, rewards, evaluation scores, and execution traces are distinct mathematical objects.

                                                                    Convention. Prompt spaces, response spaces, and laws [ftip-00IO]

                                                                      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.

                                                                      Convention. Policies and reference policies [ftip-00IP]

                                                                        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.

                                                                        Convention. Rewards and evaluation utilities [ftip-00IQ]

                                                                          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.

                                                                          Convention. Model artifacts and evaluation scores [ftip-00IR]

                                                                            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.

                                                                            Convention. Traces, states, lineages, and costs [ftip-00IS]

                                                                              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.