Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

A waiting lower bound for arbitrary initial record targets

Abstract

Arbitrary initial record labels require first-window waiting and binary depth.

Definition 1.1 (The joint original record of a literal history).

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/OriginalNarrowCost.OriginalRecord (✓ std3).

Source. Repository-derived.

Commentary.

The accepted record consists of the original low-bit-first scalar value, the literal word length modulo k+1, and the scanner’s actual final run of ones. All three coordinates come from the same word. A rejected word has record none.

Definition 1.2 (Uniform success on the whole initial free-value fiber).

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/OriginalNarrowCost.OriginalFiberFeasible (✓ std3).

Source. Repository-derived.

Commentary.

One selector receives the free initial endpoint and a chronological archive of complete issued words with their endpoint replies. At each step it either stops or appends every position of its chosen word before reading the new endpoint. The target is f of the INITIAL joint record throughout execution. Correctness quantifies every actual initial history of AllowedBlock actions in the fixed-value fiber, including every realizable initial tail. No phase or tail is revealed.

When a is true, every word chosen by the selector is internally admissible; when a is false, every complete Boolean word is allowed. The scanner still checks actual seams in either alphabet. The initial rejection stops freely with f(none). Each issued block costs one, including zero words, padding, and rejected blocks. Early stops may use less than the uniform budget d.

Definition 1.3 (Least uniform acquisition cost, with infinity allowed).

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/OriginalNarrowCost.OriginalFiberCost (✓ std3).

Source. Repository-derived.

Commentary.

The cost is the infimum in ENat of all feasible natural budgets. If there is no feasible budget, the infimum of the empty family is infinity.

Theorem 1.4 (First-window waiting plus binary discrimination).

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

Source. Repository-derived.

Commentary.

Here g=gcd(m,k+1), u=m/g, p=(k+1)/g, and h=p/u uses natural floor division. There are u tail-zero sources q(j), indexed by j in Fin u, and n is the number of distinct INITIAL labels f(q(j)). Nat.clog(2,n) is the ceiling binary logarithm; positivek denotes the positivity proof implied by k>=2. The target f is otherwise arbitrary and may depend on the INITIAL tail.

Every q(j) is realized by an actual allowed history. A successful lawful selector gives a decision tree with the same finite budget, the same complete-word actions, and the same endpoint-dependent continuation. Uniform rejection of the first word would erase all distinct labels. Otherwise its two successful replies split the label image, so one child retains at least ceiling(n/2) labels, hence at least two.

The coefficients vanish at every continuation position from m through h*m-1 for all selected phases. The sources in the chosen child have the same current value and tail. Any subsequent adaptive words therefore give a shared chronological archive for h-1 paid steps, or reject all these sources together. Uniform rejection and an early stop cannot recover their distinct INITIAL labels. After that shared prefix, binary branching needs at least clog(2,ceiling(n/2)) further words. The integer logarithm recurrence yields h+clog(2,n)-1.

No lower bound g>=2 or root first-zero condition is required. The case g=1 is included. When h=1 the quiet prefix has length zero and the estimate is the binary depth bound. The inequality also holds for targets whose cost is infinity.

References