Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Safe optimal preset acquisition

Abstract

An optimal common literal script remains safe on every original source and has an actual maximizing joint history.

Theorem 1.1 (One safe common stream and its own exact paid traces).

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

Source. Repository-derived.

Commentary.

Fix arbitrary universe-polymorphic Y and separately distinct label pairs. Labels from different values may coincide, and the independently observed bottom label is unrestricted. Both original alphabets, every original phase and inherited tail, and every unknown legal or rejected initial history are retained. The support membership image counts each phase once.

A SafePlan consists of literal words, all-phase chronological endpoint codes, their refinement of the ordered membership pair, and absence of bottom replies. For one image class choose the empty script. For two choose the binary script of the support union; the exact normalization allows either component to be empty. Three classes select the homogeneous or either internal two-label construction precisely when Pi3 holds. Four classes select the normalized safe bijective code assignment precisely when Pi4 holds. Every remaining case selects the pulse/donor three-block script. These are the existing physical constructions, including their exterior donors and safe whole-prefix seams; safety is asserted for the selected inverses.

The decoder searches the selected all-phase code and uses its own consecutive endpoint differences together with its remembered free value. Code refinement makes its INITIAL output well defined even when three-label classes split across four codes. The common words have exactly presetCost blocks. Every live original history executes that entire safe prefix; initial bottom executes none. The constant-length script bridge transports these exact selected words to a PaidTrace on the same actual source, with issued.length equal to fee(presetCost,q) and archiveWords.length equal to m times that fee. No unissued suffix is charged.

The maximizing witness is one jointly attained original state (value,phase,tail)=(0,0,0), on one original AllowedBlock history. The same history determines the initial record and its paid trace. Its block and bit fees equal presetCost and m times presetCost. The result supplies a safe attaining selector; the exact lower bounds and bit-budget equivalence are given at D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FirstWindowBoundaryPrice.

The physical scripts and refinement laws are reused from D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FirstWindowBoundaryAttainment, D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FirstWindowBoundaryCodes, D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FirstWindowBoundaryCompatibility and D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FirstWindowBoundaryFourLabels. The exact common-length trace transport is reused from D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/NearCriticalGrid. Unequal adaptive stops use the separate branch-length law at D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FirstWindowBoundaryAdaptive.

Section 28 is a direct parameter restriction H0,H1 subset of the internal phases: both boundary memberships are zero. For distinct nonempty supports Pi3 then gives exactly the odd-width two-internal-label exception; a four-label image has at least three internal classes and fails Pi4. No additional specialization theorem is needed. The broader all-k/all-m research target, tail-sensitive INITIAL labels and supports outside the first physical window are outside this result.

References