86. What a search can guarantee
On this page · Permalink · Source line 3451
The numerical proposal is one practical route. There is also a precise conditional search theorem showing why a broad class of strict curved certificates can be found without an exact conformal identity.
Proposition 77: Conditional search for strict rational curved certificates
Consider finitely many rational polynomial operator families in three coordinates, each with exact mass, and finitely many rational normalized initial states. Suppose there exists a real mass preserving invertible \(T_*\) such that every transformed initial state lies strictly inside the Lorentz cone and every transformed operator family has a common positive margin on the observation interval. Then a rational mass preserving invertible \(T\), a positive rational margin, and finite rational Bernstein witnesses exist. A dovetailed enumeration of rational transforms, positive rational margins and subdivision depths eventually finds such a witness. Whenever it returns, the witness is sound for the convex hull of the supplied families.
Read proof · Recorded Lean scope · Permalink · Source line 3455
Proof
Inversion and matrix multiplication are continuous near \(T_*\). Initial membership is strict, and the operator margin is continuous jointly in the transform, the observation, and the normalized input. The latter two range over compact sets and there are finitely many families. Thus the strict inequalities persist in a neighborhood of \(T_*\). Rational mass preserving matrices are dense in that affine matrix space, and invertibility persists in a neighborhood. Choose a rational transform there and a rational positive margin smaller than the remaining minimum. Proposition 75 supplies finite subdivisions because there is still a strict gap above the chosen margin. Enumerating all finite rational descriptions and depths eventually reaches this finite witness. Proposition 76 proves the convex-hull conclusion. \(\square\)
This is a conditional semidecision result, not a polynomial-time complexity theorem. It does not cover every valid model. Initial states on an essential boundary and families with zero margin may violate its assumptions. The implemented procedure uses a finite rationalized proposal and bounded subdivision, not this unbounded enumeration. Failure of that bounded procedure is a withheld certificate rather than a proof that no other domain works.
The theorem's uncertainty families are supplied in fixed predictive coordinates. It does not establish that those families cover an unknown generating process. It demonstrates a route from a strict robust model sector to finite machine-checkable witnesses.