Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Fixed skeleton query separation

Abstract

NativeSuppliedComparison

Fix one public full ordered skeleton S. Its chart numbers every original leaf once, in order, and its address map retains the actual depth of each leaf. The source u(S,x) fills that same chart with alpha for false and beta for true. Correct(M,S,T) quantifies every independent assignment x and every entry t from zero through T. For each there is a finite first-halt Run, and every such Run outputs the original XOR. Static(M,S,T) says that every promised Run has zero genuine Updates. Neither predicate supplies the actual lag to the controller, imposes a common runtime, or excludes unreachable Update rows.

The controller’s entire mutable state is its state word. A state selects one fixed literal or a source-blind internal instruction, a genuine Update with constant acknowledgement, or a fixed-output halt. Run retains the query state together with its absolute actual epoch. The replay theorem compares the same evolving original sources at those epochs, retaining arbitrary finite internal work. The installed query and halt sets count every state of their respective instruction types, whether or not a promised source reaches it.

Theorem 1.1 (Distinct words on each actual run).

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/NativeSuppliedComparison.same_run_distinct_queries (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each coordinate is compared with its one-label flip in the identical original chart at the identical entry. If all Read replies on the chosen run agreed, exact replay would give the same fixed halt on opposite original parities. A literal can depend only on the unique original leaf cone it enters; a literal ending inside the skeleton has no label dependence. Numbered-row locality includes absent replies. Pairwise prefix disjointness of the original cones therefore makes the chosen query states injective, even when a query state recurs at a different source epoch.

Theorem 1.2 (All installed states).

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/NativeSuppliedComparison.installed_lower_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

There are at least h query states, where h is the leaf count of S. Both original XOR values occur across the full assignment family, so two distinct fixed-output halt states are installed. The query and halt sets are disjoint. The two halts occur across assignments; they are not asserted to occur on one run.

Theorem 1.3 (Static entry cover).

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/NativeSuppliedComparison.static_installed_lower_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

For each original index and each t from zero through T, compare the all-zero assignment with its single-coordinate flip. Every separating query has actual epoch t, because that promised run has zero Updates. Removing that leaf’s own address leaves a suffix separating atomic ranks t and t plus one. The guarded atomic window places these entries among at most three consecutive ranks for a fixed suffix. Encoding an entry by its selected query and one of three offsets proves that the cone has at least r=(T+3)/3 query states. Summing over disjoint original cones gives h times r query states and two additional halts. This is a union of installed words over entries, with no assertion of h times r Reads on one run.

References