Six Birds Verified VIII: Flattening and Enablement

In plain words

A system grows by adding new ports, each answering a question about information that arrives over time. Two claims about such growth are easy to blur. One fixed program handles every stage. One fixed budget handles every stage. For one concrete family, the paper shows the first is true and the second is false. A growing host program simply extends its buffer as each port is installed, with exact costs per event. But for any budget there is a stage where more histories must be kept apart than configurations fit within it. Then some read comes out wrong, even if a new program is picked at every stage.

The second part asks about the order in which capabilities become available. On one small exact laboratory, states are grouped when each can reach the other, and the groups form an order. It is tempting to read that order as a clock that also records cost and history. It does not. A priced cycle returns the system to the same group with more time, cost and history behind it, so a state where the goal is free shares a group with one where it is costly. Two routes reach the same view at the same cost from different sources, so the route leaves a mark the present view does not show.

The two parts share one machine model: through an adapter, the laboratory runs inside the event machines of the first part. On the laboratory, the cheapest costs over paths of every length are computed exactly. Three routes reach the goal efficiently but realize only two cost values, because a cost keeps four separate coordinates with no exchange rate between them. Lean 4 formalizations accompany both parts.

What it shows

• One fixed program implements every finite stage of the growing family, causally and with exact costs.
• For every finite budget there is an explicit stage at which no one pass program within it answers every read correctly.
• A compiler between families carries feasibility forward and the obstruction backward, and not the other way.
• The enablement order carries neither cost nor history.
• Equal view and equal cost from different sources: a concrete case of purchase holonomy.

What it does not claim

Everything is finite and explicitly given: one family, one representation class, one laboratory. The capacity count is not a lower bound on time and proves no noncomputability, and a negative verdict from the finite search rules out only the class it searched. Costs are units of the model, not CPU time, memory or energy.

Cite

Tsiokos, I. (2026). Six Birds Verified VIII: Flattening and Enablement. Zenodo. https://doi.org/10.5281/zenodo.23097930