The prefix length shifts all three components of the fixed tail. The guard and scalar laws hold at every natural position, including the unobserved departure seam.
Theorem 1.3 (Complete binary capacity with a common stem).
Each of the 2^n cuts is reachable by horizon H on an actual closed-budget record. Their state-output pairs are distinct, and each output is the prefix of one fixed stem determined by its length, at most k. The encoding separates all configurations reachable on any actual record. A finite peak bound B permits at most 2^(B+1)-1 binary strings of length at most B; pairing each such string with one of k+1 output lengths bounds the entire cut family. The argument uses only the cuts and their actual reachability, so finite or infinite competing tails satisfy the same capacity statement.
Theorem 1.4 (Actual paired tails at every first disagreement).
The displayed theorem uses the following shared mathematical abbreviations, local to each fixed tuple of its parameters and candidate witnesses w1,w2. R has type (Nat->Label)->(Nat->Color)->Prop, Reach has type Nat->Configuration->Prop, and M has type Nat->WithTop(Nat). For each n and z:Fin(n)->Bool, A1 and A2 are finite label lists, a1 and a2 are Nat->Label, r1 and r2 are Nat->Color, and T(n) is a natural horizon. DecoderContracts is the conjunction of the four contracts displayed below; it includes injectivity on the union of all reachable configurations.
synchronousPrefix(P,U,z)=P++choiceBlocks(U,List.ofFn(z)). OperationRecordPredicate(o,b,closed) is the original actual record relation at the closed error budget b. The same two finite literal tails and their guard paths are chosen before every natural depth and Boolean history. Both scalar endpoints lie strictly inside their canonical hulls. Interior transport obtains actual colors for every ownership assignment at the complete six-group endpoint budget; closed-relaxation feasibility alone is not used as an owned-endpoint assertion.
LiteralTailPath and LiteralTailSplice have their complete defining formulas above. They retain the initial guard, every actual guard edge, coordinate support and affine recurrence, and exact shifted literal, scalar and guard equality with the same tail. Substituting these definitions and the shared abbreviations recovers every clause of the theorem. Empty choice histories are included. The stems agree before arbitrary k and differ at k. Safety and positionwise finite-source liveness on these target competitors force acquisition before output k, and hence finite startup; no separate startup assumption is supplied.
Equal-length block extraction gives the first-source injection. Both actual records share the entire acquired past; the first record has one fixed literal future. The common-stem cut gives 2^n<=card(states)(k+1). Joint state and output separation, with at most k+1 output prefixes, yields 2^n<=(2^(B+1)-1)(k+1) under a finite complete Peak bound B. sequenceByH(H,E) denotes the sequence H mapped to E. The encoding is injective on every configuration reachable on any actual record; all intermediate readable vertices are included. The emitted prefix is a finite external count, with readable output-side information included in the configuration.
For every H>=length(P), the bound is floor((H-length(P))/L)-1-logb(2,k+1)<=B. Natural subtraction and integer division are retained. Monotonicity fills all observation horizons, and finite or infinite peaks give liminf Peak(H)/H>=1/L. This is a necessary coefficient for each compliant decoder. The competing singleton, optional original-piece restriction and bilateral auxiliary codebook remain separate mathematical cases.