Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

NativeFibonacciActiveTable

Abstract

NativeFibonacciActiveTable

For h stages, dimension(h) is the least d with fib(d plus two) at least h plus one. The compiled Fibonacci stage path provides z(0) through z(h) at that exact dimension. The complete word is z(stage) followed by zero, accumulator, zero and four latch bits in the order L00, L01, L10, L11. Every mutable coordinate is in this one word, of width dimension(h) plus seven.

Q(i,a) uses stage i and empty latch. B(i,a,b) uses stage i and the one-hot latch at (b,i modulo two). C(i,b) uses stage i plus one, accumulator b, and that same latch. V(a,first), V(a,second), V(a,route) use stage zero, accumulator a, and latches 0100, 0101, 0001. Distinct stage words separate stages. At any shared stage, B and C use opposite parity positions. At stage zero there is no C, and B uses parity zero while both one-hot V latches use parity one. The two-hot V latch is distinct from all other latches. Both accumulator choices remain installed. This proves injectivity even for empty actual supports.

Installed is exactly the image of every Control h: two Q states at each of h plus one stages, four B states and two C states at each of h stages, and six V states. Thus the installed cardinality is eight h plus eight. When h is zero, the eight Q and V words are retained, and both Q words are halts. The nativeProgram takes immutable addresses directly, so its table and edges at h equal to zero do not depend on an uninhabited Chart zero. Actual full source trees have positive length.

At a nonterminal Q the literal is its original chart address followed by K right edges. At the pilot, alpha selects B(0,a,a), beta selects B(0,a,not a), branch holds Q(0,a), and absent selects V(a,first). At positive stages all four replies select B(i,a,a XOR chi(reply)), with chi true exactly on beta and absent. Every B performs a paid root Read: if a differs from b it selects B(i,b,b); otherwise it selects C(i,b). Every C performs a paid root Read and selects Q(i plus one,b). V first and second each perform a genuine Update, then V route performs a paid root Read and returns to Q(0,a) on every reply. Q(h,a) has fixed Stop payload a.

All words avoid adjacent ones because the stage word is legal and the accumulator has zero separators. Each nonhold typed row changes exactly one bit. Data adds one latch bit; correction changes the accumulator; stage advance uses one Fibonacci path edge; clearing removes one latch bit. The polling latch square is 0000, 0100, 0101, 0001, 0000. Only the two pilot branch rows hold when h is positive. No unsupported Read row is changed, no paid root Read is removed, and no internal instruction is inserted.

Support and EncodedSupport contain exactly the target/current-Source pairs reached at a specified complete control by an actual n-step prefix, with epoch and log existentially quantified. Their equality is proved for arbitrary entry families and includes empty supports. FirstHalt means an actual finite Run with the stated number of remaining actions and fixed payload, and no shorter terminating Run with any payload. RankDescent exposes the next actual source, epoch and single event, reduces the remaining primitive count by one, and proves a one-bit change on every finite terminating primitive. A pilot self-hold cannot occur on such a terminating Run: the same control and source would have a shorter terminating suffix, contradicting determinism. The all-row table still retains those holds.

Theorem 1.1 (Complete active word table).

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

Source. Repository-derived.

Commentary.

The statement includes minimal Fibonacci dimension, injectivity, legality, exact installed count, every typed row, actual native conjugacy, exact support equality, first-halt equivalence, and actual rank descent. The identity address map preserves the literal itself. Extra ambient cube adjacencies do not add instructions. Static constructions and comparison-class minimum-width lower bounds are outside this active construction.

Theorem 1.2 (Same-source original parity trace).

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

Source. Repository-derived.

Commentary.

The original native_active_parity_execution theorem is applied on the same full original skeleton, every independent label assignment and the same unknown entry t. Its finite guarded Run is lifted instruction by instruction to NativeSerialMachine.Run, with the same Read epoch, literal and raw reply and the same Update successor. An explicit Stop endpoint supplies the finite suffix. The exact genuine Update count is twice the difference between K and floor((t plus bit(x(0))) divided by two). The conditions are t at most twice K and either even original leaf count or t equal to zero. No claim is made for the excluded odd-entry regime. actual_register_execution certifies the same source evolution, chronological log and every literal truth. The fixed original parity payload is preserved. The existing event-cost vector is preserved in all five coordinates; no absolute three-h plus four-k plus c bill is asserted.

Theorem 1.3 (Actual Run fixes the first halt).

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

Source. Repository-derived.

Commentary.

For every control type C, native instruction function, initial control, epoch and source, any terminating actual native Run reaches its first halt at precisely the length of its complete trace, with the same fixed output. A purported shorter remaining execution contradicts native run uniqueness. The statement retains the arbitrary native machine and actual source; it requires neither a finite control carrier nor an encoding premise. The static scan uses this identity for its exact first-halt count and each remaining suffix.

References