49. Searching for a domain from observable operators
On this page · Permalink · Source line 1980
A cone certificate need not be imported from a hidden-state generator. With exact rational operators it can be searched for directly, then checked independently.
Proposition 45: Rational finite-certificate search
Suppose \(\lambda\), \(B_s\) and \(z_0\) are rational and satisfy the exact mass identities. There is an enumeration procedure that returns a valid finite certificate whenever a certificate of Proposition 39 exists with a rational normalized full-row-rank generator matrix \(V\). The procedure is sound whenever it returns. No termination guarantee is asserted when no such rational certificate exists.
Read proof · Recorded Lean scope · Permalink · Source line 1984
Proof
Enumerate all finite rational matrices \(V\) in an order that eventually includes every size and every bounded numerator and denominator range. Retain those of full row rank with \(\lambda V=\mathbf1^\top\). For each retained matrix, the requirements \(B_sV=VA_s\), \(A_s\geq0\), \(V\alpha_0=z_0\), \(\alpha_0\geq0\) and \(\mathbf1^\top\alpha_0=1\) are rational linear feasibility problems. A nonempty rational polyhedron has a rational feasible point, as follows from elimination of rational linear inequalities. These problems can therefore be decided by exact rational linear programming, or witnesses can be enumerated in a dovetailed rational search. Recheck every returned equality and sign exactly. Proposition 39 proves soundness. If a rational generator certificate exists, its finite representation is eventually considered and its feasible witnesses are found. \(\square\)
The general enumeration is a mathematical existence algorithm, not a practical complexity claim. A bounded candidate family is often the useful reference experiment. Failure within that family means only that the chosen family did not produce a certificate.
49.1 A certificate learned without hidden matrices
On this page · Permalink · Source line 1990
The observable tables of Section 38 determine the two-dimensional operators \(B_s\) and initial vector \((1,13/24)^\top\). The new reference procedure receives only these fitted operators and that vector. It enumerates intervals with rational endpoints in \([0,1]\) of reduced denominator at most eight, ordered by increasing width and then by endpoints. The coordinate restriction \([0,1]\) comes from its declared test-probability meaning.
The first accepted interval is
It uses
Every entry of every \(A_s\) is at least \(1/64\). The full per-action column sums are exactly one. These rational identities certify all word probabilities of the fitted model, not only the words used in the fit. The certificate was not supplied to the search, and no hidden generator is imported by the standalone example.
The interval is the narrowest accepted interval in this specified finite grid, not a claim of the smallest invariant interval among all real endpoints. It also need not contain every predictive state associated with an arbitrary initialization of the old hidden model. It contains the declared initial state and preserves every subsequent branch of this fitted realization, which is the requirement being certified.
The positive slack gives a robust statement: any perturbation of the lifted entries by at most \(1/64\), coupled to retain the exact per-action column sums, remains nonnegative. Interior perturbations of size \(1/128\) are used in the worked comparison. Repeated composition is valid for all horizons, while Proposition 43 bounds the changed observation law for each fixed horizon.