Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

NativeSerialDepth

Abstract

NativeSerialDepth

Definition 1.1 (Finite whole-row output representation).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeSerialDepth.RowWord

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeSerialDepth.RowWord (✓ std3).

Source. Repository-derived.

Commentary.

A finite list of optional Boolean-or-natural labels represents the complete row, including concrete exterior constructors and canonical hole class labels.

Definition 1.2 (Injective preorder row encoding).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeSerialDepth.rowWord

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeSerialDepth.rowWord (✓ std3).

Source. Repository-derived.

Commentary.

Each leaf is one tagged label and each binary constructor is a separate marker. Prefix parsing proves injectivity without a tree-size bound; the encoding is used to transfer the original effective finite-output service to the complete canonical row.

Theorem 1.3 (Full original-service depth and whole-output image).

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

Source. Repository-derived.

Commentary.

The original selector simulation feeds the unrestricted native depth and prefix-free output-image theorems. The domain remains the entire ActualFiber, with one shared finite selector state at the actual epoch N and initial physical register substitution iterated N times on u. The common state may encode the complete retained row, task input, accessible workspace and any genuinely retained prior chronological record. It is not identified with H: H retains mixed-epoch Read constraints, while the selector appends the new chronological external suffix. Under original 59.3 the complete takeover state is a deterministic function of common input and R and recovers R; original 62.2 gives equal reached state on the same actual continuation record, and 74.1 exhausts accessible source information by U. Consequently this single state is common to the full fiber, rather than adding an extra producer-record filter. The frozen canonicalRow_record_iff, rowFiberEquiv and historyCellEquiv identify R with the complete exterior/full partition and H with its literal constraints, retaining all cross-class disequalities, repeated occurrences and absent guards. Producer acquisition records excluded by 59.3 are never reinstated. Certified N at least every historical epoch is an allowed specialization of this stronger unconstrained-N theorem. Injective finite row coding yields equality of whole canonicalRow and literalRecord, and at most four to the K terminal whole rows, including K zero and root/empty cuts. The proof-only image decoder supplies no runtime oracle. The original partial selector has sourcewise finite executions; no common local-work, runtime, update, workspace or address bound is assumed.

Theorem 1.4 (Labeled native trace and full-output uniqueness).

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

Source. Repository-derived.

Commentary.

Two NativeSerialMachine.Run proofs from the same program, control, epoch and source have equal complete labeled traces and equal full outputs. The original statement and induction are preserved. OriginalVector.InterleavedWordRecovery consumes this theorem for the constructed vertex and word runs; it adds no execution interface or unlabeled halt semantics.

Definition 1.5 (Complete original-prefix agreement).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeSerialDepth.OriginalAgree

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeSerialDepth.OriginalAgree (✓ std3).

Source. Repository-derived.

Commentary.

Agreement quantifies over every original address of length at most the given radius and uses the actual four-valued readout, including absence.

Definition 1.6 (Proof-only descriptor selection).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeSerialDepth.descriptor

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeSerialDepth.descriptor (✓ std3).

Source. Repository-derived.

Commentary.

A finite replay, when it exists at a Read boundary, determines its unique epoch and physical address. A classical default on other words is used only to form a finite image. It supplies no effective stationary service.

Theorem 1.7 (Finite actual physical support).

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

Source. Repository-derived.

Commentary.

Four-valued reply words of length strictly less than K form a finite set. Actual Read boundaries are uniquely determined by these words, so their physical epoch-address descriptors lie in one finite set. This does not assume finite control, a finite source fiber, bounded addresses or bounded update counts.

Theorem 1.8 (Finite original observation depth).

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

Source. Repository-derived.

Commentary.

Take the maximum address length in the finite physical support, with maximum zero for an empty support. All-epoch original-prefix locality makes every physical reply agree on sources with the same original prefix. Actual execution transfer then preserves the entire local/update/read trace and complete output. The radius can depend on the program, common input, fiber and initial epoch; no bound depending only on K and no common radius for all initial epochs is asserted.

Theorem 1.9 (Whole actual row and record).

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

Source. Repository-derived.

Commentary.

The domain is the entire NativeHistoryCells.ActualFiber of the complete old canonical row and mixed-epoch history. All old inequalities, repeated classes and absent-cut guards are retained by that interface. The conclusion concerns the complete new canonicalRow and the independently computed literalRecord, including exterior and whole partition. Arbitrary finite cuts, root and empty cuts, and finite nonempty fibers remain included. No ground-binding or unification premise occurs. The result is valid even without nonemptiness, and at every fixed actual common epoch.

Theorem 1.10 (Encoded effective serial clause implies finite depth).

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

Source. Repository-derived.

Commentary.

Apply the exact encoded-service inclusion to the full actual fiber and whole-row output. Sourcewise stopping and one uniform chronological Read budget then give precisely the finite-original-depth implication, without any stationary-service construction or other direction of the four-way classification.

References