A Notation and hypotheses
On this page · Permalink · Source line 2406
Letters are local to a section. In particular, \(A\) denotes required premises in a proof field, but a matrix in the binary examples. The type declarations, not the letter alone, determine the object.
| Symbol | Meaning |
|---|---|
| \({\mathcal P}\), \(V\), \({\mathcal J}\) | A declared proof field, its nodes, and its justifications. |
| \(A\), \(L\), \(T_0\) | Required premises, admissible leaves, and requested targets, with \(A\subseteq L\). |
| \((K,H)\) | Selected nodes and certified justification records. Only usable rules contribute to derivability. |
| \(D_{\mathrm{cert}}(K,H)\) | The least certified closure in the selected record. |
| \({\operatorname{Anc}}_L(T_0)\) | Backward ancestry expanded only outside the admissible leaves. |
| \(\mathcal M_F(U)\) | Local models on patch \(U\) satisfying all certified rules supported entirely in \(U\). |
| \(\Gamma(\mathcal M_F)\) | Coherent families of those local models under restriction. |
| \(\operatorname{cl}_F(S)\) | The least declared rule model containing the positive observations \(S\) and all admitted leaves. |
| \(\operatorname{Ext}_F(S,N)\) | Rule models containing \(S\) and avoiding the negative observations \(N\). |
| \(F_{\mathcal U}\) | The same field with only rules whose entire supports appear in a covering patch. |
| \(Q(a)=(q_i(a))_i\) | The joint task representation, least in retained distinctions for its task family. |
| \(\mathscr A\), \(C\), \(q\) | A class of possible archives, an encoding scheme, and a task on that class. |
| \(P_K(S)=S\cap K\) | Pure retention of records selected by a fixed mask. |
| \(D:E\to R\), \(p:E\to S\) | A linear defect and a protected observable. The repair condition is \(Dy=0\), \(p(y)=p(x)\). |
| \(H=\ker D\cap\ker p\) | The ambiguity space of a nonempty protected fiber. This \(H\) is not a set of justifications. |
| \(U_M(S)\) | Weighted target reach from the mandatory starts and a selected supplement, in a fixed directed bridge graph. |
| \(n_{\mathrm{eff}}\) | A real, variance-equivalent review count in the specified covariance model. |
Assumptions that change the conclusions
On this page · Permalink · Source line 2438
The unique-core theorem uses backward expansion that stops at admissible leaves and proves a least pair of record sets. The compression results quantify over a whole archive class with one decoder for each task. Weighted domination counts only targets reachable before deletion. The greedy ratio requires a positive cardinality budget, with zero and saturated budgets handled separately.
Whole-support gluing is sufficient when the patches cover all nodes and every complete certified rule support. More generally, node coverage and entailment of every original rule by the visible rules are necessary and sufficient for universal gluing. Merely covering pairwise dependencies is not sufficient in general. The linear alternative requires a field. General algebraic functionals need not be bounded under an added topology. The information formula requires a finite field, a finite-dimensional feasible affine fiber, and a uniform distribution.
Endpoint equivalence fixes the complete assumption context. A refinement chain preserves the chosen tasks only when the corresponding recovery condition holds. The unrestricted positive-rule model always contains the full node set as a model. Nonempty global model spaces can still have empty prescribed extension fibers. Provenance change detection distinguishes information lost during serialization from collisions of different serialized bytes.
The review mean is unbiased only when its error means vanish. Its effective count requires positive marginal variance and positive variance of the mean. A minimum-variance aggregate allows real weights and assumes a known positive definite covariance matrix. No probability of mathematical correctness follows from these assumptions alone.