Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Uniform Legal Terminal Law

Abstract

Adaptive first-hit fair-bit sampling is uniform on native legal terminal words.

For each native live state, CompletionCount counts literal legal completions of the remaining actual output length. The empty layer has one word. The next false branch has count C(maxTrue,q); a true branch, when fuel is positive, has count C(fuel-1,q). Their sum is the current count. With zero fuel the true branch is forbidden.

Theorem 1.1 (Adaptive composition and the uniform completion law).

Proof. Machine-checked in Lean as D5/S0/Tower/DBonacci/TerminalSamplingLaw.terminal_sampling_uniform_law (✓ std3). ∎

Source. Repository-derived.

Commentary.

At every fixed first-accepted draw (t,x), the consumed cursor is cursor+(t+1)(q+1). Its event depends only on the finite source prefix before that cursor. Native replay identifies the continuation event with an event of the unused suffix. Independence of these disjoint iid coordinate families proves exact event factorization on the same tape.

Nat denotes natural numbers, Words(h) is Fin h to Bool, C(m,f,h) is completionCount and mu is fairTape. Return is the event that sample returns the displayed word with some finite final cursor. Draw fixes the first accepted retry and integer. Legal is native runAdmissible=true. ConditionalFairWordMass is the mass of the singleton word under the iid fair Fin h word measure conditioned on that native legal set. AtLeast compares integer values; subtraction is natural subtraction. The four displayed rows hold jointly, for every listed parameter.

A returned-word event is the disjoint union over accepted branch integers and retry indices of the corresponding draw-and-continuation events. Summing over retries gives integer mass 1/C. There are exactly C(next) accepted integers selecting the requested next bit. Induction on the remaining output length cancels C(next) against the continuation mass 1/C(next). The resulting path mass is 1/C(initial), including the empty terminal word and forced-zero branches.

For maxTrue=k-1 and initial fuel=k-1, the native full-budget count is dbonacci k (N+2). Every legal length-N word therefore has mass 1/G_N, and every illegal word has mass zero. The same returned-word law equals the iid fair length-N word law conditioned on native legality. All branch choices use the concrete fair-bit rejection evaluator; infinite retries are exceptional. The state retains N’s remaining output budget and does not define a stationary law on tail state alone.

References