Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Saturated four-label first-window boundaries

Abstract

Four distinct membership labels have exact two-block compatibility on the complete original first-window source.

Theorem 1.1 (The phase-once pivot and safe Pi4 construction).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FirstWindowBoundaryFourLabels.original_first_window_four_label_compatibility (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fix m>=5, k=2m-2 and P=ZMod(2m-1). The arbitrary supports H(0),H(1) lie in B={1,…,m}; ell is their ordered membership pair. Its full image has four labels. The output labels A(v),B(v) differ separately for each free value, while all cross-value coincidences remain allowed. Y is an arbitrary type, without a finite-type hypothesis, and the separately observed bottom label is arbitrary. The theorem retains both original alphabets, every actual value and phase, all legal inherited tails, and unknown legal or rejected histories.

multiplicity(m,H,z) is the number of phases with ell(j)=z. Its domain is the phase set itself, so each phase contributes once; histories and tails do not repeat a contribution. pivot is the sum of ell(j) over all phases in the pair vector space. Since 2m-1 is odd, one or three multiplicity parities are odd. The first conclusion identifies pivot as the unique label whose parity differs from the other three. It includes both parity patterns. Pi4 means that erasing this label from the internal image leaves at most one label, and that an internal base occurrence forces the pivot to be base.

Necessity uses the actual common scheduled rows. Equal row pairs refine both membership coordinates, including sources with different stopping times. Four labels exhaust four binary codes. Choosing one representative per label gives an injective, hence bijective, code map; surjectivity then forces every phase of one label to have that same code. This no-splitting statement uses four labels. It imposes no corresponding restriction on three-label families.

For a bijection g of the four pair vectors, the sum of g(ell(j)) is g(pivot). This follows by grouping the phases by their four labels and using the odd total multiplicity. Both physical rows are even, so g(pivot)=00. The second row is zero on U={2,…,m-1}, leaving only codes 00 and 10 internally. Thus at most one internal label differs from the pivot. If base occurs internally, its second bit is zero there and its first bit is zero at exterior phase zero; its code is therefore 00 and bijectivity forces pivot=base.

For sufficiency the internal labels together with base and the two boundary labels fill the four-label set. Select a bijection with pivot code 00, first bit zero on base and second bit zero on the internal image. Its normalized boundary codes additionally satisfy the displayed seam disjunction. When the pivot differs from base, base has code 01, so every exterior phase, including m+1, has second charge one. When the pivot is base, the normalized last boundary has first charge zero, giving a zero-ending root before a possible all-one successor. These are the normalized alternatives of 29.20-29.22.

S contains exactly those internal phases whose selected first bit is one. BaseAssignment has flip=0, exterior equal to the selected base second bit, donor=0, and the selected codes at phases one and m. The phase sum is zero by g(pivot)=00. Expanding its first coordinate gives the first displayed row-parity equation; expanding the second counts m-1 exterior phases and the two boundaries, giving the second equation. The actual baseCode equals g(ell(j)) at every phase, including both boundaries, phase zero and every exterior donor.

baseWords is the ordered prefix-parity inverse of these two even physical rows. The root begins zero and clears every inherited tail. The seam disjunction means the successor begins zero, has a zero at literal index one after its leading one, or enters from a zero-ending root. In the middle case the root tail is at most m-1 and the leading run adds at most one, below k=2m-2. In the last case an all-one length-m successor is safe because m<k. Thus the entire two-block prefix succeeds for every original source. The exact base_script_code supplier establishes its own consecutive endpoint differences.

Each source inverts the bijection from its own acquired differences, then uses its remembered free value to select A(v) or B(v). A single literal stream serves both values; no archive or output is borrowed from another source. Initial bottom stops freely. Every live displayed script has two acquired blocks and 2m emitted bits. These script counts do not themselves establish an exact optimal PaidTrace price, an adaptive branch price, or the equivalent boundary rows of table 29.6.

The physical inverse, normalized code and inherited-tail seam execution use D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FirstWindowBoundaryCompatibility. Actual common-row necessity uses D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FirstWindowBoundaryCodes. Phase support sums use D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FirstWindowBoundaryAttainment. Actual histories and one common preset stream use D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/DonorCorrection.

References