KBonacciIrreversibleAcquisition
Abstract
Complete actual-history first-zero acquisition classification and uniform cost.
Theorem 1.1 (Complete original first-zero acquisition theorem).
Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/KBonacciIrreversibleAcquisition.whole_first_zero_acquisition (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every k>=2, m>=1, either full or internally legal block alphabet, arbitrary label type Y and initial record target f on the actual SourceRecord subtype Q, six conclusions hold. actualSourceTarget extends f outside Q using f(bottom). Only Q participates in acquisition. SourceRecord is exactly the image of one actual finite block history from the empty word, including bottom and every joint value-phase-tail record. Uniform RecordAcquired is equivalent to the two root FirstZeroCriterion conditions A_0(0,P) and A_1(0,P). Every acquired target has a controller of horizon D+1+L, where D=floor((k-1)/m) and L=phaseCost; its initial bottom branch stops with f(bottom), an empty archive and zero issued blocks. When m>=2 this horizon equals D+p. For every raw initial history target F, HistoryAcquired is equivalent to factorization through historyRecord by some uniformly acquired record target. Finally the actual successful all-one archive has exactly prefixRecords with h=k-tm and the same-history phase filter I_i(theta)=b_i; the current value is v+sum b_i and the current tail is s+tm, while the target still uses initial v,theta,s. The initial current reading freely selects a tree. Each later action uses only its attained complete-block endpoint. There is no resetting, source copying, internal-bit reading, target observability or decidable equality assumption. The statement is not an optimal-cost claim for L.