Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Four-label table extremes

Abstract

The extreme rows of the expanded four-label table are exact on the complete original source.

Theorem 1.1 (One internal class and three-or-more internal classes).

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

Source. Repository-derived.

Commentary.

Fix m>=5, k=2m-2 and the full original first-window family. The two supports are retained as ordered membership pairs, so cross-value label coincidences do not identify distinct membership classes. The theorem keeps arbitrary Y, both original alphabets, all actual INITIAL phases and inherited tails, and the original complete-block feasibility contract.

The existing four-label compatibility result supplies the exact original feasibility iff Pi4. The table isolates two extreme rows. If the internal image has one class, the erase of any pivot has cardinality at most one. The full image has four classes, so the internal class cannot be the base: otherwise the boundary phases and the exterior base could supply at most three classes. Hence the base clause of Pi4 is vacuous and Pi4 holds.

If the internal image has at least three classes, erasing any one pivot leaves at least two classes. This directly contradicts the first Pi4 clause, whether or not the pivot lies in the internal image. The proof uses the actual phase image and its finite-set cardinality; it does not enumerate literal words or replace the physical source by an unrestricted parity query.

The full-image decomposition is proved from the actual phase partition into exterior, boundary and internal phases. The saturated compatibility theorem is stated at D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FirstWindowBoundaryFourLabels.

Theorem 1.2 (The exact price of one common literal stream).

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

Source. Repository-derived.

Commentary.

The full image counts each phase once. One class is equivalent to two empty supports. With two classes, every member of the union carries one nonzero membership pair; each component support is either empty or that union, and at least one equals the union. This includes equal supports and an empty value fibre. Cross-value coincidences of output labels do not merge membership pairs.

The price is zero for one class, binaryCost of the support union for two classes, and two or three for three and four classes according to Pi3 or Pi4. In the four-class branch, one internal class always gives two, whereas three or more internal classes give three. The same literal stream serves both free values; stopping and decoding use each source’s own archive.

For the joined one-block obstruction, two phases with the same actual root charge produce the same component label at each remembered free value. Their ordered membership pairs therefore agree. The full image injects into the two possible charges. This uses jointly realized original histories at tail zero, without assuming that the two component decoders stop together.

The upper bounds use the safe binary, boundary-compatible two-block, and pulse/donor three-block constructions. The lower bounds quantify every legal common stream and stopping rule, including early stops and rejecting blocks. OriginalPresetFeasible uses unknown actual histories, immutable INITIAL targets, both alphabets and arbitrary inherited tails. An initially rejected history has its independent bottom label and stops at zero. The theorem gives the minimum block budget; each issued block has exactly m bits by the chronological archive-length law.

The binary and three-block physical constructions are supplied by D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FirstWindowBoundaryAttainment; the two-block relations and safe selected inverses are supplied by D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FirstWindowBoundaryCompatibility and D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FirstWindowBoundaryFourLabels.

The component lower bounds use the actual adaptive law at D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FirstWindowBoundaryAdaptive. All four expanded rows use phase-once multiplicities. For K={0,z}, the two boundary-only labels each occur once; the pivot is zero precisely when the internal z class is odd. When K has two classes and excludes zero, the complement has two labels, zero and z. Their multiplicity parities are equal precisely when the pivot lies in K. The exterior phase partition has m-1 phases plus each boundary outside K, giving boundaryParity. A minimizing common selector also has a jointly realized original history whose actual trace attains the minimum; every trace counts only emitted blocks. The exact bit budget is m times that minimum.

References