Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Independent binary support branches on the full original source

Abstract

Safe original binary branches stop and pay at their own lengths.

Theorem 1.1 (The exact adaptive budget and chronological fees).

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

Source. Repository-derived.

Commentary.

Fix m>=5, k=2m-2 and T=2m-1. The output universe is arbitrary, with separately distinct labels at each free value and arbitrary cross-value coincidences. The support may differ between free values. Every INITIAL phase and inherited tail remains in scope, and the legal or rejected history and its length remain unknown.

For a finite support J the branch fee is the length of that branch’s binary word list. The optimal adaptive budget is max(binaryCost(H(0)), binaryCost(H(1))). The remembered free value chooses the branch once. The selector stops when that branch’s own list has ended; it emits no word belonging to the longer branch.

The decoder compares the acquired consecutive endpoint differences with the binary codes at actual phases. Code equality preserves membership in that branch’s support. Empty supports have empty scripts and stop immediately; the independent bottom label also stops without a block. For every actual history, the paid trace contains exactly the selected binary words, and its block and bit lengths are binaryCost(H(v)) and m*binaryCost(H(v)) when the INITIAL record is live, and zero when it is bottom.

The lower bound applies the zero-block and nonempty one-block necessities at each arbitrary remembered value. The auxiliary target agrees with the original target on that same actual fibre, so neither a value-zero-only root lemma nor a shared branch length is assumed. All issued words are complete length-m blocks and are legal in either original alphabet since m<k.

The binary code, inverse words, boundary compensation and full-tail safety come from D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FirstWindowBoundaryAttainment. The script selector uses the existing branch stream and stopping definitions at D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/NearCriticalGrid. Each branch is transported through original_final_script and trace_congr, with its own actual INITIAL record and own chronological archive; the constant-length grid trace lemma does not supply the unequal stopping lengths.

The exact bit budget is m times the block budget. A maximizing value is selected, and the whole-source realization theorem supplies one actual history with INITIAL phase and tail zero at that value. The same history and issued archive attain both worst fees. The adaptive classification is the stated individual-fibre supplier applied to the two free values. The retained relation here is its exact original-history implementation with independent branch stops. The common-stream GLOBAL law and its expanded four-label parity table are separate statements.

References