Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Complete saturated actual cones

Abstract

Saturation exhausts actual child event fibers and prevents cycles, shared children and shared next-reading targets.

The Controller and Correct structures describe one stationary table on ZMod(pP), with p at least two, P positive, and a first action that reads. Each initialized input follows its original physical run to a fixed correct output. A slot consists of an actually used reading control and a physical digit. events(u) contains every pair of original input and physical time at that slot, including repeated visits by the same input. readIndex(e) counts reads up to and including that event. At a common read deadline h, mass(u) is the sum of two to the negative remaining read allowance over this entire event set.

The actual Edge relation joins consecutive reads on the same original input, with only actual waits in between. Reach is its reflexive transitive closure; Loop is its transitive closure from a slot to itself. Halting at a slot means that its fixed read successor halts immediately. A ConeTree expands all actual children at each fork and retains a singleton event at each terminal leaf. leafCount and internalCount count its leaves and forks. Neither unique incoming edges nor absence of cycles is a premise.

Theorem 1.1 (Complete child transport and distinct actual targets).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/SaturatedActualCone.result (✓ std3). ∎

Source. Repository-derived.

Commentary.

Encode each actual future by one binary symbol per subsequent read. The actual successor set has at most two elements. If one complete future answer word is a prefix of another, their terminal labels and initial events agree. Thus these binary words are distinct and prefix-free. Kraft’s inequality gives the complete slot mass bound. Advancing every event of a saturated active slot doubles its mass and injects it into at most two complete child fibers, each of mass at most one. Both fibers must have mass one, and positivity excludes every omitted event. Literal waiting tails give a common positive delay. This complete transport raises the minimum read index and identifies the sole predecessor of each child. Consequently the whole successor cone has no cycle or reconvergence. An initialized input cannot return to a saturated slot, so the original-input projection is injective on every complete cone fiber. At a terminal slot the complete event fiber is a singleton; mass one forces its read index to equal h. Equality in the mass bound also forces every represented original run to use exactly h reads. When p is at most three, two pairs of child digits at a common reading control intersect, so predecessor uniqueness identifies their parent slots. Every next-reading target differs from the initial control. Strict growth of the minimum read index constructs a finite complete binary expansion. Exhaustive event transport preserves counts across forks, giving m leaves and m minus one forks when the entrance has m events.

This statement covers two and three physical digits, and retains the original positive waiting durations. It treats an initial read (ell = 0), so a positive common initial waiting prefix is outside its model. An ordering of leaves by original low phase and its leaf-depth correspondence and the gap-cost inequalities are additional assertions.

References