Exact acquisition cost of a coprime phase singleton
Abstract
Coprime nonzero initial phase singletons have exact safe complete-block cost.
Theorem 1.1 (The least budget is the maximum of two and the paid arrival time).
Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/CoprimeSingletonCost.coprime_nonzero_singleton_cost (✓ std3). ∎
Source. Repository-derived.
Commentary.
Feasible, Selector, Archive, output and execute denote the original NarrowWindowCost objects. OriginalRecord is the original scanner record. Proof arguments are suppressed. The bounded get operation uses its displayed strict index bound, and the archive map projects each AllowedBlock to its word.
For every k>=2, 2<=m<k, gcd(m,k+1)=1 and 1<=j<=k, the INITIAL phase index j receives label B and every other index receives label A. The label type, distinct A and B, initial-bottom label and free value v are arbitrary. For either complete-block alphabet the least raw feasible budget is max(2,ceil(j/m)). The lower bound ranges over all adaptive selectors, including selectors whose actions reject.
One attaining selector and its endpoint trees witness this same budget. Initial rejection stops freely with the bottom label and an empty archive. Every legal INITIAL tail returns the INITIAL singleton label, and every recorded endpoint is some value. At each strict archive prefix the selector issues its recorded complete word; on the complete archive it stops with that INITIAL label. For every actual initial history the raw execution, tree result and charged archive length agree.
Literal root and repair words provide the near cases. Remote targets use paid zero blocks, a pulse and a final word; empty waits and zero final padding are included. Actual initial histories are realized in the original scanner, and every raw feasible selector induces an endpoint tree.
The universal endpoint-tree obstruction in D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/CoprimeSingletonLower combines absorbing rejection, even one-block charge and indistinguishability before paid arrival. The same literal marker equations also govern the attaining root, repair and pulse words.