Six Birds Verified VIII: Flattening and Enablement

Abstract

A growing interface acquires new information one port at a time. This paper separates two claims about such growth that are easily run together. For a family of read and flip ports whose bits are acquired from time-released sources, one fixed program, the growing host, implements every finite stage causally and faithfully, with exact costs per event. Yet no single finite information budget suffices for all stages. For every budget b there is a stage at which 2n acquired histories must be told apart, while at most M(b) complete configurations fit within b, so no one-pass program within b answers every installed read correctly. A stage-uniform compiler carries feasibility forward and this obstruction backward, and not conversely. The second part studies the order in which capabilities become available, on one small exact laboratory. Mutual reachability of successful paths orders the classes of states, but neither cost nor history descends to this order: a priced cycle restores a capability while extending time, cost and history. On the same laboratory the all-length cost front is computed exactly, and two routes with equal current view and equal cost but different sources give an operational instance of purchase holonomy. Lean 4 formalizations accompany both parts.