Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Exact additional prices on actual full-positive children

Abstract

Exact additional prices on actual full-positive children

Definition 1.1 (One original source at one acquired archive).

Lean statement: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.OperationalRequest

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.OperationalRequest (✓ std3).

Source. Repository-derived.

Commentary.

A request retains the immutable INITIAL record and current record of the same original history, its remembered free output and its whole acquired archive.

Definition 1.2 (The whole actual child).

Lean statement: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.ChildRequests

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.ChildRequests (✓ std3).

Source. Repository-derived.

Commentary.

The child contains exactly all original allowed histories matching the free output and the entire chronological archive. Histories at the same phase may have different original tails and lengths. No independently reachable coordinates are substituted for this fiber.

Definition 1.3 (Both original alphabets).

Lean statement: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.SelectorLegal

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.SelectorLegal (✓ std3).

Source. Repository-derived.

Commentary.

Every selected complete word respects the selected original alphabet. In the critical width m less than k all m-bit words are internally legal; their seam can still reject.

Definition 1.4 (One child-local literal suffix).

Lean statement: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.PresetPolicy

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.PresetPolicy (✓ std3).

Source. Repository-derived.

Commentary.

The selected suffix is indexed by additional paid archive length from this actual acquired offset. Stops and decoding depend on the source own complete endpoints. No compatibility with another child or free-value fiber is required.

Definition 1.5 (Correct stopped continuations and paid budgets).

Lean statement: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.RequestFeasible

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.RequestFeasible (✓ std3).

Source. Repository-derived.

Commentary.

One lawful selector returns f of the INITIAL record on every actual request through a stopped paid trace within the additional budget. Remembered INITIAL bottom has its independent free label. Newly reached bottom remains absorbing under the original bit updates. Every complete issued word, including rejection, costs one.

Definition 1.6 (Attained least finite budgets).

Lean statement: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.BudgetPrice

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.BudgetPrice (✓ std3).

Source. Repository-derived.

Commentary.

The price is the infimum of all feasible natural budgets in the extended naturals. An empty feasible set has infinite price. The exact price theorem exhibits a feasible least natural budget.

Definition 1.7 (Adaptive additional fee).

Lean statement: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.ChildAdaptivePrice

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.ChildAdaptivePrice (✓ std3).

Source. Repository-derived.

Commentary.

The adaptive price ranges over every lawful original selector on this whole actual child, with arbitrary own-endpoint stops and literal words.

Definition 1.8 (Preset additional fee).

Lean statement: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.ChildPresetPrice

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.ChildPresetPrice (✓ std3).

Source. Repository-derived.

Commentary.

The preset price restricts the same feasible domain to a single literal suffix chosen for this acquired child. The already paid prefix is excluded.

Theorem 1.9 (Every original adaptive competitor).

Lean statement: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.full_positive_lower

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

Source. Repository-derived.

Commentary.

Let odd m be at least three and k=m+1. An actual positive child with full support equal to its parent window and one immutable label per surviving phase has at most 2 to the power h distinct labels under any correct original continuation of additional budget h. The actual parent inverse earns common tail one. Actual histories representing labels are selected only for counting; correctness still includes every matched original history. Common-tail compression and the existing exact binary leaf bound supply the inequality for arbitrary actions, waits, repairs, early stops and uniform rejection.

Theorem 1.10 (The actual many-label suffix).

Lean statement: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.full_positive_many_attains

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

Source. Repository-derived.

Commentary.

For at least three distinct labels, the original physical INITIAL decoder supplies donor-compensated literal words of length d=ceil(log2 n), their exact paid traces and final-endpoint decoding. Its same attained script is made into a preset policy at the acquired archive length. The regular seam and the d=2,n=4 alternative, including m=3, are supplied by the physical decoder. No new question port, clearing block or independently chosen branch stream is introduced.

Definition 1.11 (The exact binary obstruction).

Lean statement: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.BinaryException

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.BinaryException (✓ std3).

Source. Repository-derived.

Commentary.

In coordinates translated by the actual paid index, one label occupies precisely vertices m and m-2 and a different label occupies every other surviving vertex. In absolute coordinates this is H={u+m,u+2m} modulo m+2, where u=am. The translation is a calculation from the known issued count.

Definition 1.12 (The four exact cases).

Lean statement: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.fullFee

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.fullFee (✓ std3).

Source. Repository-derived.

Commentary.

The fee is zero for one distinct label, two for the exact binary obstruction, one for every other two-label table, and ceil(log2 n) for at least three labels. It counts the distinct label image on actual support rather than phase occurrences.

Theorem 1.13 (Original adaptive and child-preset minima).

Lean statement: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/FullPositiveWindowPrice.original_full_positive_price

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

Source. Repository-derived.

Commentary.

For every actual acquired archive with the full positive support, both original alphabets and every repeated-label INITIAL table satisfying the per-phase label law, one literal child-preset continuation attains fullFee. Every correct original adaptive competitor pays at least that fee. Consequently the two original additional prices both equal fullFee. The same actual history supplies INITIAL labels, current phase, current scalar and inherited tail.

The parent is the actual alternating word beginning and ending in one. Its internal zero earns inherited tail one from every surviving original history. The current phase is INITIAL phase plus (a+1)m. These facts come from full_positive_history_trace; positivity without full support is insufficient.

For a nonconstant binary table the next actual window misses only the vertex m-1 of the child. Its label fixes response zero. The unique non-source donor in that next window compensates parity, and the existing prefix-parity inverse gives a complete literal word. An inverse containing a zero is safe from inherited tail one. The all-one inverse is unsafe exactly for the stated H partition. This is the original shallow classification, with every one-block action tested against the same actual histories.

In the exception the complete zero word is issued and paid at a+1. It clears the inherited tail and gives no label information. The complete word 110 followed by m-3 zeros is then issued at a+2; its charge is exactly H, its leading run two is safe from zero, and the final endpoint returns the INITIAL label. Both words belong to the one actual suffix and cost two.

A constant table stops at the acquired endpoint. The many-label lower bound gives h at least ceil(log2 n), while the physical suffix attains that integer. For binary tables it also rules out zero fee; the separate all-action exception proof supplies the stronger lower bound two. These conclusions concern one actual acquired child and do not give a GLOBAL stream across unrelated siblings or an exact price for every full INITIAL target.

References