Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Actual endpoint operators and complete windows

Abstract

Classify actual Boolean-word endpoint transfers, complete-window products, and their faithful transfers with absorbing rejection over every field.

Fix any field K and an integer k at least two. The live states are the integers from zero through k-1. A false bit resets a live state to zero. A true bit increments it when the result is below k and otherwise rejects. Rejection is absorbing. Words are finite Boolean functions read in increasing coordinate order. List.ofFn preserves their length and every coordinate; conversely, a list is exactly List.ofFn of its own coordinate function. In the display, arithmetic on Fin k states uses their natural values, and natural subtraction is truncated at zero. Finite families use image and card for image and cardinality. The get operation on an option is used only in branches where that option is present. The matrix unit denotes the identity on the indicated state space.

The run from live state s agrees with the original runAdmissible scanner with maximum fuel k-1 and initial fuel k-1-s. A word is DBonacciAdmissible exactly when its run from zero accepts. The live transfer L_w has column s equal to the basis vector at the actual terminal state, or the zero column on rejection. The totalized transfer retains one additional rejection basis state, represented by none, and sends every column to its actual terminal basis vector. These are column-input matrices.

Theorem 1.1 (Endpoint composition, exact families, and faithful totalization).

Proof. Machine-checked in Lean as D5/S1/Words/AdmissibleWords/KBonacciActualEndpointOperators.actual_endpoint_operators (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a word containing a false bit, let p and t be the lengths of its initial and final true runs. If its run from zero accepts, both endpoints are below k, their sum is strictly less than the complete word length, and the run from any state s ends at t exactly when s+p is below k. Thus L_w=E(p,t)=e_t r_p^T, where r_p(s) is one for s+p below k and zero otherwise. If a word rejects from zero, it rejects from every live input.

Reading u and then v gives L_(uv)=L_v L_u. For two arbitrary length, zero-containing words accepted from zero, the displayed endpoint product is their actual composition. The composed run from s accepts exactly when both t_1+p_2 and s+p_1 are below k, and then ends at t_2. When t_1+p_2 reaches k, every input rejects.

At width m=k+1, every accepted word contains a false bit. The possible endpoints are exactly p,t below k with p+t at most k. The actual word consisting of p true bits, m-p-t false bits, and t true bits realizes each pair. Its length is exactly m, with every false bit retained. The all-true width-m word rejects and induces the zero live matrix. Endpoint matrices are nonzero and distinct over every field. There are N_k nonzero one-window operators and N_k+1 one-window operators in total.

For every k at least three, the windows with endpoints (k-1,0) and (0,k-1) compose to (k-1,k-1), outside the one-window domain because its endpoint sum exceeds k. For k=3 these actual windows are 1100 and 0011. Consequently the one-window family is not closed under composition for any k at least three.

For every positive integer r, every actual word of length r*m induces either rejection or one of the k squared endpoint matrices. Conversely, any pair (p,t) is realized by the two full windows (p,0) followed by (0,t). The entire family generated by positive numbers of complete windows is therefore exactly all endpoint matrices plus zero, is closed under multiplication, and has k squared plus one elements. This includes k=2.

Allowing r=0 adds exactly the empty-word identity. Every nonempty complete-window operator has rank at most one, whereas the live identity has rank k and k is at least two. The resulting monoid is closed under multiplication and has k squared plus two elements.

The faithful lift Gamma sends A to the matrix whose live block is A, whose live rows in the rejection-input column are zero, whose rejection row in live column s is 1 minus the sum of A’s column s, and whose rejection diagonal entry is one. Gamma is injective, preserves identity and multiplication, and the actual totalized word transfer is Gamma(L_w). In particular Gamma(0) is e_bottom times the all-one row and is nonzero. The rejection-input column always stays at rejection.

The totalized one-window, positive-window, and empty-inclusive families are exactly the respective Gamma images. They have the same three operator counts, the generated families are closed, and the same two actual windows witness one-window nonclosure when k is at least three. These counts concern operators, not historical states.

Adjoining a final false bit to any original admissible n-coordinate word preserves admissibility, gives exactly n+1 coordinates, and ends the actual run at zero. Zero resets the tail while remaining an actual position; endpoint parameters never remove internal positions.

References