Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Binary Selector Recut Fibers

Abstract

A binary selector relation has exact nonlinear recut fibers, attaining reconstruction labels and supplied-action separators of length at most m+2.

Theorem 1.1 (Original relation and complete residual classification).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/BinarySelectorRecutFibers.selector_residual_classification (✓ std3). ∎

Source. Repository-derived.

Commentary.

For each natural m, Word(m) consists of binary lists of length m. A parameter p=((i,j),b) indexes the word ij0i when b=false and ij1j when b=true. The relation is exactly the union of those two families. Every word has length 3m+1, the relation is nonempty and finite, and its cardinality is 2 times M squared, where M=2 to the power m. The results include m=0; the nonlinear recut comparison below assumes m at least one.

In the displayed formulas val is the underlying list of a fixed-length word, false and true denote 0 and 1, pair and Prod denote the indicated ordered pair and product type, concat is ordered list concatenation, cons adds a first symbol, singleList(b) is [b], and nil is the empty list. card is Nat.card, and the displayed ratio is rational. derivative(t,S) is the language of f for which concatenating t with f belongs to S. predecessorMap(m) sends (i,j) to S(i,j).

At cut 2m every actual prefix is ij, and at cut 2m+1 every actual prefix is ijb. Conversely all these prefixes are actual. Ordered concatenation and the prescribed component lengths uniquely recover i, j and b. These are controlled prefixes with a completion in this same relation; the state carries no immutable full-word tag.

The predecessor residual S(i,j) is exactly the two-word language containing 0i and 1j. Its derivatives at 0 and 1 are the singleton languages containing i and j. Equality of predecessor residuals therefore recovers both components. The predecessor residual image consists of exactly M squared different S(i,j), while the current residual image consists of exactly the M singleton languages containing x as x ranges over all m-bit words.

The original StrictAnchoredBoundary state for ijb with one deletion credit is (ij,[b]), and its boundary is fine(p)=(S(i,j),[b]). The zero-credit image is exactly the pairs (singleton(x),empty); the one-credit image is exactly the range of fine. These equalities describe actual joint images, with no free-product assumption.

Theorem 1.2 (Actual widths, fibers and behavioral minimum).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/BinarySelectorRecutFibers.selector_widths_and_fibers (✓ std3). ∎

Source. Repository-derived.

Commentary.

For m at least one and selector cut k=2m+1, the actual zero-credit boundary image has M points and the one-credit image has 2 times M squared points. Their rational ratio is 2M. A current fiber is the subset of the latter image whose derivative through its one-symbol tail is singleton(x). A fixed-bit fiber also prescribes that tail as [b].

For each x, the current fiber is in bijection with pairs (b,y), where y is the unused m-bit component. rebuild(x,0,y)=((x,y),0) and rebuild(x,1,y)=((y,x),1). Its fine images are exactly the two disjoint families (S(x,j),[0]) and (S(i,x),[1]), of total cardinality 2M. At each separately supplied b the cardinality is M. No empty or unrepresented fiber contributes to these counts.

The strict anchored specialization applies directly with alphabet Bool, source length 3m+1, relation C and admissible type (2m+1,1). On actual states, equality of legal supplied-action languages is equivalent to equality of boundaries. Its strict Option transition equation gives the original moving-anchor append and fixed-anchor delete updates, including missing edges. Every exact representation maps uniquely and onto this actual boundary image; its actual one-credit image therefore has at least 2 times M squared points, and the boundary attains that minimum.

The zero-credit actual image of any exact representation has at least M points by the same strict anchored specialization at type (2m+1,0). In the displayed factor equations, subtype arguments denote their underlying states and labels are inserted into their canonical actual ranges. mapTypeBoundary maps a successful state to its public type and boundary and preserves a missing transition.

Only labels at a supplied public type are counted. The cardinalities assign no cost to the relation description, a transition table, intermediate computation, initialization, a physical device or a retained archive. An accessible source record must be included in the joint representation before a width claim is made.

Theorem 1.3 (Sharp supplements and attaining encodings).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/BinarySelectorRecutFibers.selector_optimal_supplements (✓ std3). ∎

Source. Repository-derived.

Commentary.

For any finite label type Z and any label map L on the actual one-credit points, reconstruction from the current selected component and L requires at least 2M labels. If the selector bit is also supplied, reconstruction requires at least M. The selected component is equivalent to the singleton current residual, and the point parameters are in bijection with the original actual boundary image, so these are lower bounds on the original fibers.

The minimum rollback alphabet theorem is applied to the selected-component map and to the selected-component-plus-bit map. Their maximum fibers are 2M and M, respectively. Exact rollback is converted to joint-record injectivity by the frozen injectivity criterion, with a nonempty actual carrier.

The attaining label is L(ij0)=(0,j) and L(ij1)=(1,i). Given x and (b,y), rebuild returns the actual boundary parameter and therefore the original anchored boundary. With b separately supplied, only y is retained. binaryLabel concatenates b with the m supplied bits of y, and binaryRecover uses its head and tail to reconstruct p. Thus these maps attain m+1 and m binary bits.

The displayed selectedJoint(m,L) is the map p to (selected(p),L(p)); selectedBitJoint(m,L) is p to ((selected(p),p’s selector),L(p)). These joint records use the selected word itself, equivalent to its singleton current residual.

For every proposed fixed binary length ell, an injective joint record using ell-bit labels exists exactly when ell is at least m+1, or at least m when the bit is given. The ceiling logarithms of the sharp label cardinalities are correspondingly m+1 and m. The theorem quantifies over arbitrary finite Z, rather than presupposing the optimal alphabet.

Theorem 1.4 (Short lawful supplied-action experiments).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/BinarySelectorRecutFibers.selector_legal_separators (✓ std3). ∎

Source. Repository-derived.

Commentary.

experiment(p,c,x) requests deletion of p’s current selector b and then appends c followed by all m bits of x. Under the original StrictAnchoredBoundary.step and legal definitions for this same C, the full experiment is legal exactly when x is i for c=0 or j for c=1. The proof checks actual extendability at every append and exact full-length membership at its endpoint. After deletion the controlled prefix is ij, so supplying a new selector chooses a different branch of the same relation.

For unequal fine boundaries, if the bits differ separator requests the deletion of the first bit, which exists exactly on the first side. If the bits agree and the i-components differ, it uses experiment with c=0 and the first i. Otherwise the j-components differ and it uses c=1 and the first j. Each branch experiment has one delete and m+1 appends, hence length m+2. The first state has every requested edge; the other misses an edge. A separating experiment is supplied explicitly, with no enabled-action query, failure output, hidden-symbol read or credit replenishment.

Complete actual-prefix classification transports these separators to every pair of actual states of type (2m+1,1) with unequal original boundaries. The final clause gives an action word of length at most m+2 legal on exactly the first side, and the earlier clauses give its concrete construction.

Theorem 1.5 (Full branching and the missing predecessor relation).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/BinarySelectorRecutFibers.selector_full_branching_sharpness (✓ std3). ∎

Source. Repository-derived.

Commentary.

The family attains the full-branching formula N1=2 times N0 squared with N0=M. For a known selector 0, all S(x,j) differentiate to the same singleton(x), while the original predecessor residual varies injectively with j. This is the missing predecessor relation: the current residual and fixed bit retain no record of which j was paired with x.

The displayed fixedFirstPredecessor(m,x) is the map j to S(x,j), with x fixed and j ranging over every m-bit word.

For every natural K there is an m at least one such that the one-credit actual width exceeds K times the zero-credit width. The parameter and relation vary in this claim. Every individual C remains finite, with the exact cardinality above. The value alphabet stays Bool and the common action names stay append 0, append 1, delete 0 and delete 1.

Theorem 1.6 (Failure of an alphabet-only same-cut bound).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/BinarySelectorRecutFibers.result (✓ std3). ∎

Source. Repository-derived.

Commentary.

AlphabetOnlyTwoBound asserts the same-cut inequality N1 at most 2 times N0 for every m at least one. At m=1, the exact widths are eight and two, so that assertion is false. This refutation concerns the same selector cut, and does not contradict a comparison of peaks taken over all cuts.

The forward right-language interpretation is the standard one for finite prefix automata, as in Daciuk, Mihov, Watson and Watson, Incremental construction of minimal acyclic finite state automata, sections 2 and 3, Computational Linguistics 26(1), 2000. That source supplies the forward meaning only; it does not supply deletion credit or the recut fiber counts. The nonlinear selector classification and lawful separators here are mathematical consequences of the stated binary relation and strict supplied actions.

References