42. Finite tests give an outer hierarchy, not automatic closure
On this page · Permalink · Source line 1720
Define the test cones
Each \(C_h\) is polyhedral because it is an intersection of finitely many homogeneous half-spaces. It need not be a pointed cone or have a bounded normalized base.
Proposition 38: Test-cone hierarchy and a finite stopping certificate
The cones satisfy
Their intersection \(C_\infty\) is the largest cone contained in \(C_0\) and invariant under all \(B_s\). If an exact equality \(C_{h+1}=C_h\) occurs, then \(C_h=C_\infty\) and the finite inequalities certify all future word probabilities. If the representation is observable, meaning that the rows \(\lambda B_w\) span \(E^*\), then \(C_\infty\) is pointed and \(\lambda\) is strictly positive on its nonzero elements. If reachable vectors \(B_wz_0\in C_\infty\) span \(E\), the cone is also generating.
Read proof · Recorded Lean scope · Permalink · Source line 1731
Proof
For a first symbol \(s\) followed by a word \(v\), \(B_{sv}=B_vB_s\). The inequalities for all words of length at most \(h+1\) are therefore exactly the displayed recurrence. If \(z\in C_\infty\), every test on \(B_sz\) is another test on \(z\), so \(C_\infty\) is invariant. Conversely, invariance of a cone contained in \(C_0\) makes every successive test nonnegative, hence places it in \(C_\infty\). Equality at one finite step establishes invariance immediately and therefore gives the intersection.
If both \(z\) and \(-z\) lie in \(C_\infty\), every test row annihilates \(z\), so observability gives \(z=0\). For \(z\in C_\infty\) with \(\lambda z=0\), sum word probabilities along any fixed action sequence. Mass conservation makes the sum zero. Every term is nonnegative, so every word test vanishes and again \(z=0\). Spanning by reachable cone elements gives the final assertion. \(\square\)
A useful negative witness is a state admitted by the current inequalities and a specific longer word with negative proposed probability. It demonstrates that this state needs to be excluded. It does not prove that the initial state, or every reachable state, is invalid.
Finite stabilization is sufficient, not promised. Even three predictive coordinates can require a nonpolyhedral domain, as Section 51 shows. Checking a long list of trajectories is not the same as checking the invariance identity that makes every trajectory valid.