Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

The first LOWER selector on the attained physical bank

Abstract

A supported first LOWER selector with paid SMALL costs and an exact depleted complement.

The setting is the centered doubling source on all original physical labels Fin(k), as defined by OriginalLowerFullBank.OriginalSource. Put N=2^k-1, Q=2^(k-2), C=(2^k-2)/2=2Q-1, q=2^L and H=2q. The actual source, extrema, signed own rows, negative SMALL nonET witness and power branch are unchanged. This result has the additional scope m>5, e=1, 4<=F<=H/4, y<=2b-3, a0>=2b+1, floor(E/b)<=q-3 and E mod b>(y-1)/2, where E=(N+z-2a0)/2. The original source implies b<=y. The row-eight seed a0 is its actual source value; no a0<=z or five-pair closing identity is imposed.

SourcePrefixInventory supplies the row-mask weights and finite SMALL ordering. OriginalLowerFullBank.canonical_lower_full_bank constructs Pfull and its exact bank Kfull, retaining the entire positive b row. Write G=H/4, delta=b-n=HDelta, tau=F/2 and kappa=(z-n)/2. Its retained n and w masks have weights A and G-A, its retained z mask has weight c, and its u row is full. The original charge equation is 2(height(Pfull)+charge(Kfull))=z+y. Pfull begins with x, has no duplicate physical label and has every natural take in [0,C].

Theorem 1.1 (Literal supported selection and the next physical prefix).

Lean statement: D5/S3/Combinatorics/Circle/OriginalLowerFirstSelector.canonical_lower_first_selector

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/OriginalLowerFirstSelector.canonical_lower_first_selector (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every source in the stated corner, the theorem constructs submasks Nsel of Sn and Wsel of Sw, a mask Bsel in the full b row, and a natural payment p in the actual row eight with p<=2^(sourceLength 8)-1. Their physical union Hsel is a subset of Kfull. With M=(y-1)/2, it proves 0<=rho=E-p*a0-charge(Hsel)<=M. The output FirstStep exposes all masks, Pfull, the ordered post batch and their complete bounds. No selector conclusion is a hypothesis.

The source forces the actual row-seven length to be L-1 and a0=N-qy. Put dw=w-b and eta=2taudw-b. The original row recurrences and the actual B1 terminal imply 0<eta, 4eta<b and eta<2taudelta, while canonical minimality gives A<=tau. The literal retained w mask contains its low mask of weight tau-A and its single tau bit. Numerical reflected weights are used only to choose subsets of these already available physical indices.

For ell=floor(E/b)M, set epsilon=b-r. If the retained low w bits reach epsilon in reflected dw weight, the first crossing selects them with overshoot at most M-1. Otherwise the single tau w bit works when its weight is at most epsilon+M. In the remaining case the canonical strict ceiling proves A*delta<=M, and a first crossing among the retained n bits supplies the correction. The selected b coefficient is ell+weight(Nsel)+weight(Wsel)+1, and is proved at most q-1. Every reflected correction therefore pays its actual b compensation.

For ell>=tau, the source implies y-b>eta. The integer star=(tau+1)b-tauw lies in (0,M], with M+star>=b, so it corrects every remainder above M using the actual retained tau bit and a paid b mask. To leave enough b budget, set B=(q-tau-1)b. If E<B, pay zero. Otherwise choose the least natural p with E-B+1<=pa0. The actual row-eight LARGE terminal proves Q<=f0a0 for f0=2^(sourceLength 8), while ceiling arithmetic proves pa0<Q. Thus p<f0 and the payment is literally available. The modified E-p*a0 is nonnegative with quotient at most q-tau-2. No future positive row is spent and no empty-row support is assumed.

The specified SMALL batch is Bfirst=(Kfull minus Hsel) union fullRow7 union bitsRow8(p). Its positive charge is (q-1-weight(Bsel))*b+(G-1)*y. Its negative magnitude is (A-weight(Nsel))*n+(G-A-weight(Wsel))w+cz+(tau-1)u+pa0. All differences are proved mask complements. The earlier B1 and v costs were paid in Pfull; the whole y row and every unheld b label are paid here. The finite SMALL ordering theorem orders exactly Bfirst between legal endpoints, using the original bound Q-1 on each SMALL label.

Append V0=sourceParent 8 and then U=sourceParent 7 individually. Their actual values satisfy 2s(V0)=N-a0 and 2s(U)=y-N. Before V0 the height is (a0-y)/2+rho; after V0 it is (N-y)/2+rho; after U it is rho. Each height is proved in [0,C]. The resulting P1=Pfull++post++[V0,U] is Nodup, begins with x and has every natural take in [0,C], including overlength takes saturated at rho.

The exact unused complement is Hsel union bitsRow8(complement of the paid mask) union {sourceParent 9} union fullRow9 union {sourceParent 10} union fullRow10 union laterLabels(11). Here laterLabels(start) is the union of each actual parent and its full own row for start<=i<2m, excluding the boundary x. The row-eight remaining weight is exactly f0-1-p. Parents 9 and 10 are distinct from x, and parent 2m equals x. This partition is proved from physical injectivity and set subtraction; equal source values never identify labels and prepaid bits never reappear.

This is a local prefix result in the circle configuration problem of Damasdi, Frankl, Pach and Palvolgyi, Monochromatic configurations on a circle, arXiv:2504.10687v2, Conjecture 3.1, DOI 10.5070/C6.68671. It leaves arbitrary depleted-tail viability, actual terminal arrival, all-m completion of both power branches and original normalization open. A legal prefix and conserved charge do not assert legal exhaustion of its remaining labels. The construction is a new synthesis of supported crossing, source-forced prepayment and physical inventories; it makes no literature novelty claim.

References