Exact Selector Family Profile
Abstract
The literal binary selector relation has exact forward and one-credit profiles on its full actual carriers.
Theorem 1.1 (Exact selector-family profile).
Proof. Machine-checked in Lean as D5/S3/ObserverMemory/NonlinearSelectorProfile.exact_selector_family_profile (✓ std3). ∎
Source. Repository-derived.
Commentary.
For each m at least one, C(m) consists exactly of i ++ j ++ [false] ++ i and i ++ j ++ [true] ++ j, where i and j are binary lists of length m. Every word has length 3m+1. Words(h) is the set of binary lists of length h. R(m,k) is residualSet(C(m),k), using completion residuals of actual prefixes. Q(m,k,d) is image(C(m),(k,d)) from StrictAnchoredBoundary, with the same actual prefixes, moving anchors, supplied actions and remaining credit.
The displayed selectorPair sends ((i,j),b) to ({false::i,true::j},[b]); copyPair sends (a,r) to ({a::r},[a]). singleton(r) denotes the language containing only r. Thus both range equations describe realized joint images and exclude additional pairs. After the selector and ell copied symbols, forward residuals are precisely all singleton suffixes of length m-ell. With positive ell and one credit, the anchor residual contains the newest symbol followed by that suffix, and the actual tail is exactly that newest symbol.
At preparation cuts, complete each prefix to two blocks using a common binary padding. If the completed first blocks differ, select false and copy the first block. If they agree, the second blocks differ; select true and copy the second block. The same completion is accepted from one prefix and rejected from the other. This proves distinct residuals for every binary preparation prefix, including cut zero and cut 2m. Every such prefix is extendable.
The strict anchored specialization supplies the actual joint-image equation and its finite sum over admissible tails. During preparation every anchor residual admits both one-symbol tails, giving the same count 2^k at credit one. At the selector the two first-symbol branches recover both blocks, and either selector bit is realized, giving 2 times (2^m)^2 points. After copying begins, the singleton residual and its first symbol determine exactly the joint point shown in copyPair. The terminal forward residual is the singleton empty word; the terminal one-credit image still distinguishes the last copied bit.
K0(m) is the maximum of card(R(m,k)) over 0 <= k <= 3m+1. K1(m) is the maximum of card(Q(m,k,d)) over the same cuts and 0 <= d <= min(1,k). The Lean definitions use finite suprema over exactly these integer ranges. Zero-credit images have exactly the forward residual count by the original supplier, so they are included in K1. There is no type (0,1). The forward maximum is attained at preparation cut 2m; the one-credit maximum is attained at selector cut 2m+1.
clog(2,N) is the ceiling binary logarithm of the finite label count N. The strict anchored specialization makes these counts the least conditional capacities for the supplied action contract. The peak binary widths are 2m and 2m+1, differing by one. At the selector alone the widths are m and 2m+1, differing by m+1. These are full-carrier counts conditional on an already supplied public type; they assign no acquisition, initialization, computation, transition-description or physical-memory cost.