Sharp finite-alphabet one recut
Abstract
An actual predecessor is determined by its complete finite-alphabet derivative table.
Theorem 1.1 (Actual carriers, sharp bounds, and simultaneous realization).
Proof. Machine-checked in Lean as D5/S3/ObserverMemory/SharpFiniteAlphabetOneRecut.sharp_finite_alphabet_one_recut (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let A be any finite alphabet of cardinal q at least two. A language C is a nonempty set of words all of one length n. For every natural j, P_j=pref(C,j) is the set of length-j prefixes having a completion in C; R_j=residualSet(C,j) is the set of their actual residual languages R(v)={f: vf belongs to C}. At every cut 1 <= k <= n, let N=card(R_k). The theorem derives that C, every P_j and R_j, each residual in R_j, the one-credit boundary and all of its fibers are finite, and N is positive. It includes both k=1 and k=n.
For a residual S and letter b, derivative(S,b)={f: bf belongs to S}. The actual one-credit carrier oneBoundary(C,k) consists precisely of (S,b) with S in R_(k-1) and derivative(S,b) nonempty. forward(S,b)=derivative(S,b) always belongs to R_k on this carrier. The fixed fiber fixedFiber(C,k,E,b) is {S in R_(k-1): derivative(S,b)=E}; currentFiber(C,k,E) is {(S,b) in oneBoundary(C,k): forward(S,b)=E}. Thus the first cardinality is exactly h(E,b), without counting multiple prefixes that share a residual.
StrictIdentification gives an equivalence e from oneBoundary(C,k) onto the existing strict image(C,(k,1)). It sends (S,b) to (S,[b]); its forward residual is exactly the strict recut {f: [b]f belongs to S}, and its letter projection is the singleton tail [b]. This is an identification of actual images in both directions. In the displayed formula recut(S,t) denotes {f: tf belongs to S}. No independently chosen residual and tail are added to the carrier.
For each actual E in R_k and each b in A, h(E,b) <= (N+1)^(q-1), the whole forward fiber has cardinal at most q(N+1)^(q-1), and the entire one-credit carrier has cardinal at most qN(N+1)^(q-1). FullBranching(C,k) means that every actual extendable prefix v of length k-1 permits vb for every letter b. Under this condition the corresponding bounds are N^(q-1), qN^(q-1), and qN^q. The condition quantifies over all actual prefixes of the same C.
Since k-1<n, no actual preceding residual contains the empty word. Such a residual S is therefore recovered from the entire function b maps to derivative(S,b). Each entry is empty or an actual member of R_k, and every entry is actual under full branching. Fixing derivative(S,b)=E leaves the q-1 coordinates indexed by letters different from b. Restricting to these coordinates is injective on the fixed fiber. The same reconstruction gives injective finite encodings for the whole forward fiber and carrier. This proves the bounds without replacing the actual image by a presumed exhaustive table universe.
For simultaneous attainment fix any prescribed N>=1 over that same A. Choose an embedding of Bool into A. Transport the original optional-index word encoding word(i), for i in Option(Fin N), through this embedding. Denote the transported word by e(i); it has length N and is injective in i. Enumerate the finite alphabet once. For a table t:A to Option(Fin N), its anchor v(t) concatenates the q blocks e(t(a)) in this fixed order. Every anchor has length qN. Equal-length block cancellation and the original encoding injectivity recover each entry from its anchor.
A table is admissible in the unrestricted family when at least one coordinate is some s. In the full family every coordinate must be some s. Define the single literal language C in each regime to consist of exactly v(t)b e(some s), over all admissible t and all b,s satisfying t(b)=some s. Its length is qN+1+N, and its cut is qN+1. A positive N gives a constant table and an actual word, including when N=1. All blocks and all words lie in the original alphabet A; additional letters outside an embedded binary pair occur as selected letters and independent table coordinates.
The actual length-qN extendable prefixes are exactly the anchors v(t) of admissible tables. Their residuals are exactly S(t)={b e(some s): t(b)=some s}. Taking derivatives recovers the optional coordinate payloads, so t maps to S(t) injectively. The actual length-(qN+1) prefixes are exactly v(t)b with t(b)=some s; their residuals are the singleton languages {e(some s)}. Conversely every such table and selected coordinate has its stated literal completion. Thus there are exactly N current residuals and no extra preceding prefixes, residuals, or current prefixes.
The whole one-credit carrier is exactly {(S(t),b): t admissible and t(b)=some s for some s}. For a fixed actual singleton E={e(some s)} and a fixed letter b, all remaining coordinates are free: Option(Fin N) in the unrestricted family and the nonempty optional indices in the full family. Filling the selected coordinate with some s gives a bijection onto the actual fixed fiber. The fixed-fiber cardinalities are (N+1)^(q-1) and N^(q-1); summing over all q letters gives the current-fiber equalities. The same filling construction maps triples (s,b,r), with r the remaining-coordinate function, bijectively onto the entire actual one-credit carrier. Both directions use the exhaustive boundary classification. Injectivity recovers b, the full table, its selected index s and every remaining coordinate. Counting this whole-carrier bijection gives the total equalities. All three equalities therefore hold simultaneously in each one language. The complete preceding-prefix classification also proves full branching at every actual preceding prefix of the full family.
The attainment quantifiers are every finite A with q>=2, every positive N, every actual E, and every b in A. Each regime uses one language for all its equalities. Lengths and cuts may depend on A and N; attainment at each separately prescribed length and cut is outside this assertion. The full total qN times N^(q-1) equals qN^q because q is positive.
The strict supplied append and credit-limited deletion interpretation is the one of strict_anchored_specialization with d=1, the same C and the same k. Its legal-action equivalence and minimum exact boundary factor therefore apply through the explicit carrier equivalence. For the existing minimum_rollback_alphabet, use the actual finite source oneBoundary(C,k), first with the observation (forward,b) and then with forward alone. Its maximum fibers are respectively the maxima of h(E,b) and of card(currentFiber(C,k,E)); the theorem above computes their sharp values. This concerns the supplemental alphabet for exact recovery, rather than a total machine or physical memory cost.
The original binary one-recut result supplies the optional-index encoding and the literal-language precedent. The recursive right-language signature ingredient is described by Daciuk, Mihov, Watson and Watson, Incremental Construction of Minimal Acyclic Finite-State Automata, Computational Linguistics 26(1), section 2, pages 4-5. Radionova and Okhotin, A hierarchy of reversible finite automata, arXiv:2411.14538v1, Definition 2, supplies reversibility terminology. These sources are not attributed the finite-alphabet extremal constants proved here, and no worldwide priority claim is made.