Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Two adjacent low-tail labels

Abstract

The threshold-three immutable target has original adaptive and preset price Q+1 at odd width and Q+2 at even width.

Definition 1.1 (The immutable initial target).

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/TwoAdjacentLowTailLabels.initialLabel (✓ std3).

Source. Repository-derived.

Commentary.

For k=Qm, the four entries of labels are A, B, C and R. Bottom is an arbitrary separately known label, without a distinctness condition. A legal INITIAL record with tail at least k-3 receives R. At smaller INITIAL tails its phase j=(-phase).val receives B at one, C at two and A elsewhere. The free scalar value is immaterial to this label map. The target of the updated record is never substituted for this INITIAL target.

Theorem 1.2 (The extra block at every even width).

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

Source. Repository-derived.

Commentary.

Assume Q is at least two, m is at least four and even, and labels is injective. Every feasible original adaptive budget d is at least Q+2. OriginalAdaptiveFeasible quantifies one lawful selector over all actual complete-block histories, both free values and every legal INITIAL tail. The alphabet parameter includes both original Bool control alphabets. Early stopping and absorbing rejection remain part of the original execute recursion.

Compare actual INITIAL tails k-4 and k-3 with the same phase and value. Their targets differ. A first zero before position three merges them; a first zero after position three, or an all-one root, rejects both. Correctness therefore forces exactly three leading ones followed by zero. The remaining root suffix is unrestricted. Joint original-history realization supplies these complete records.

Follow the single chronological archive with zero endpoint differences. Phases one and two have zero root response. Before index Q all later windows miss both phases. They retain a common scalar and current tail. Different labels B and C exclude stopping and uniform rejection at every earlier node. Thus this archive is traversed by actual sources under the controller’s own chosen actions.

If all outside INITIAL phases were screened during these Q blocks, every strictly interior outside vertex of each window would have response one. At the root, the three forced leading bits and the zero at position three, followed by those required interior differences, force its last bit to zero at even width. To screen the shared boundary the next block must start with one. Its required alternating interior differences force its last bit to zero again. Induction leaves the final phase k unqueried, contradicting complete screening. Consequently some outside INITIAL source survives. Its phase can depend on the policy and need not be m.

That survivor, B and C traverse the same acquired archive, with the same scalar and current tail. They have three distinct immutable labels. A remaining budget of at most one block admits at most two different successful endpoint differences; rejection is uniform for their common tail and cannot separate them. The original own-charge separation theorem therefore rules out every total budget at most Q+1.

The policy-dependent survivor is used on the actual lower-bound path; no fixed outside phase is assumed.

Definition 1.3 (The first final query).

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/TwoAdjacentLowTailLabels.queryWord (✓ std3).

Source. Repository-derived.

Commentary.

The one is at local index one; all other bits are zero.

Definition 1.4 (The even-width final query).

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/TwoAdjacentLowTailLabels.finalWord (✓ std3).

Source. Repository-derived.

Commentary.

The one is at local index zero; all other bits are zero.

Definition 1.5 (The literal attaining stream).

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/TwoAdjacentLowTailLabels.attainingWords (✓ std3).

Source. Repository-derived.

Commentary.

For a local index i<m, rootWord is true exactly when i<3 or i is even. The middleWord bit is true exactly when i has parity one at even m and parity zero at odd m. The queryWord has its only one at index one; finalWord has its only one at index zero. Thus at odd m the stream is 111(01)^((m-3)/2), Q-1 copies of (10)^((m-1)/2)1, and 01 followed by m-2 zeros. At even m it is 1110(10)^((m-4)/2), Q-1 copies of (01)^(m/2), 01 followed by m-2 zeros, and 1 followed by m-1 zeros. Repetition exponents count literal pairs. Every displayed block is paid.

Definition 1.6 (Decode the acquired original archive).

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/TwoAdjacentLowTailLabels.archiveDecoder (✓ std3).

Source. Repository-derived.

Commentary.

Compatibility means that some original phase and tail s<Qm, with the given free value, produce exactly this scriptArchive. chosenRecord selects one such record. The decoder returns its INITIAL target; if no compatible record exists it returns bottom. Archive separation proves that all compatible records have the same INITIAL target. The choices use only the acquired chronological archive and the remembered free scalar.

Theorem 1.7 (Exact prices and the same-history paid trace).

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

Source. Repository-derived.

Commentary.

Let Q be at least two, m at least four and labels injective into an arbitrary universe-polymorphic type Y. The arbitrary bottom label need not differ from any entry. The alphabet parameter includes both original Bool alphabets. Set fee=Q+1 at odd m and fee=Q+2 at even m. Both global prices equal fee. The original complete-block prior includes all phases, both scalar values, all legal INITIAL tails, the empty history and rejected histories.

In the trace formula flattenHistory concatenates the literal bits of the given initial history. The policy stops with bottom on a free rejected observation; otherwise it follows finalSelector for the displayed stream and then applies archiveDecoder at the remembered free value. Its issued archive is empty on initial rejection and the actual scriptArchive on every legal record. The PaidTrace, exact issued word list, paid length and execute equality all refer to this same history. The returned value is the immutable initial label. positivek denotes the positivity proof supplied by the displayed hypotheses.

The root rejects precisely INITIAL tails at least k-3. Its acquired charge and all later legal charges are differences of consecutive actual endpoint readings. The first Q blocks have zero support exactly {1,2} at odd width and {1,2,m} at even width. Any earlier positive scan difference belongs to A; root rejection belongs to R. At index Q, queryWord has the actual INITIAL mask {0,1}, so it identifies B. At odd width the remaining zero identifies C. At even width the remaining pair is C at phase two and A at phase m. The finalWord at index Q+1 has INITIAL mask {m-1,m} and separates these two sources. No root suffix or intermediate support is substituted for INITIAL phases.

The root contains zero at position three and leaves tail at most m-4. Every following word contains zero at local position zero or one. The internal-zero execution theorem proves all actual seams legal for k=Qm; absorbing rejection and the exact literal tail are retained. QueryWord and finalWord end in zero. Their trailing zeros are literal paid symbols. There is no unpaid clearing, reset or time displacement.

For the baseline lower bound the existing original_cost_lower theorem is applied to the three distinct tail-zero labels A, B and C, with gcd(m,Qm+1)=1. Its first-window wait is Q and its binary depth is two, giving Q+1. The even-width actual-policy survivor theorem supplies the extra block. The original script-preset construction supplies the upper bound; preset inclusion and the adaptive lower bound yield both exact global prices. For Q=2,m=4 the literal list is 1110|0101|0100|1000 and fee four. For Q=2,m=5 it is 11101|10101|01000 and fee three.

References