Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

StationaryHistoryCore

Abstract

Unrestricted actual slot incidence selects structural core targets and literal-tail baselines.

B is the image of all binary histories under nextTarget. Its multiplicity at q counts all binary parents targeting q; s sums multiplicity minus one over B. Thus |B|=N-s. Select exactly s targets from G minus B. For each selected q choose an actual pure resolving row with target q. Core is B union selectedTargets, extras is Targets minus Core, and e=|Targets|-N. Every history on a pure resolving row is unary. The selected rows are distinct because their target identities are distinct.

Theorem 1.1 (Exact controller-derived core and extras).

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

Source. Repository-derived.

Commentary.

These sets and all their counts are obtained from C/I. A further exact equivalence readStateEquiv identifies the finite readStates image with the original ActualRead type. No supplied forest, N-core, read-count, injection, or J/s/Xi equation is a premise.

Theorem 1.2 (Distinct selected resolving rows).

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

Source. Repository-derived.

Commentary.

The selected row’s actual next-target identity recovers q, giving injectivity. Their cardinal s is consequently bounded by the already derived resolving-row count J.

For every internal history n the positive representative is 1+((delay(n)-1) mod P). A binary history has representative strictly below P; an internal unary history can have representative P. BinaryBaseline(q) is the maximum of all binary-parent representatives targeting q, with empty maximum zero. Baseline(q) uses this value on B, the selected resolving row’s literal wait on selectedTargets, and one elsewhere. TargetRead identifies an actual nonfirst target with the original NonrootRead type. Tail(q) is actualL of that target, the maximum of actual positive literal arrivals. These definitions have no score function parameter.

Theorem 1.3 (Literal-tail bounds for all baselines).

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

Source. Repository-derived.

Commentary.

Every selected parent’s actual indexed run constructs an Arrival in the original controller. The canonical actualL maximum bounds its literal delay and hence its positive representative. Supremum over all binary parents preserves the bound; selected resolving baselines remain literal waits, and extra baselines remain one.

BackgroundParent(n) holds exactly when n is binary or row(n) is the selected row of a selected resolving target. These alternatives cannot coincide. BackgroundChildren(q) retains each full history n targeting q whose unique forest parent is a background parent. BackgroundDigits(q) is its color image, and k(q)=3-|BackgroundDigits(q)|. Only this digit occupancy takes an image: the history collection retains all different prefix identities, including equal-row histories with equal literal waits.

Theorem 1.4 (Actual core digit occupancy).

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

Source. Repository-derived.

Commentary.

A binary parent supplies two distinct child digits. A selected pure resolving row supplies its two distinct actual outgoing target digits through all of its unary histories. Thus every core has k in {0,1}; extra targets have no background. Different histories have disjoint original (x,i) event sets even if an ancestor and descendant contain the same original label.

References