Papers · Preprint
Six Birds Verified VI: The Price of an Interface
Changing how a system is described has no single price, and cheaper looking shortcuts can be unsafe to prune.
In plain words
When a coarse view of a system fails to support a law, there are standard ways to repair it: look at more, predict less, or merge states. This paper asks what a repair costs, and when a search over routes to a repaired view can safely throw a route away. In a four state example there are four exact repairs, priced on eight axes such as width, look ahead and lost distinctions. None is cheaper than another on every axis, and none fits a budget that the unrepaired view meets.
So a change of interface has a quote, the set of repairs that cannot be beaten on every axis at once, not a price. The quote does not fix which route is chosen, the purchase history, or the value of one more unit of budget. Width and look ahead are separate costs: two systems both need width 16, one at look ahead 15 and one at 4. For a family of noisy deterministic systems, a cheaper, inexact option becomes acceptable exactly when the allowed error reaches a sharp threshold.
Part II is about pruning. Keeping the cheaper of two partial routes that look the same can discard the only route that finishes, for example when the dearer one has paid for a permission. The paper uses a stronger test: can every next step from one be matched from the other at no greater cost? This test is computable and safe, though not necessary, and a solver built on it returns a witness for every minimal cost up to a length bound. Most results are formalized in Lean 4, with the exceptions listed.
What it shows
- A four state example with four incomparable exact repairs, none within budget.
- Width and look ahead are independent costs of a refined view.
- Noisy deterministic systems have a sharp tolerance threshold for repair.
- A computable, safe pruning test and a solver that finds every minimal cost up to a length bound.
What it does not claim
The pruning test is sufficient, not necessary, and the solver's guarantee is up to a length bound. Positive weighted sums of the costs can miss efficient options, and some results, such as the entropy formula, are not formalized in Lean.
Cite
Tsiokos, I. (2026). Six Birds Verified VI: The Price of an Interface. Zenodo. https://doi.org/10.5281/zenodo.23097922