Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

NativeUniformInput

Abstract

Fixed native common input and cell factory

CommonCode is the product of the existing rowWord constructor list, the lexicographically sorted finite Q address list, the existing chronological mixed-epoch history codes and N. The four reply codes remain 0,1,2,3. Contradictory and unreachable finite histories remain computation inputs. The decoder and cell factory are uniformly primitive recursive before quantification over old rows, Q, H and N. Numeric old class names are preserved, including gaps and repeated occurrences; names are never replaced by dense class ranks. The exact depth is the current requiredDepth. This stage does not decide feasible cells, run the unifier, compute the ground-binding criterion or budget, or certify the whole controller.

The matching Reg mirror proves typed whole-family reconstruction, variation, role sensitivity and actual observational dependence on the complete infinite domain. Contract source-selection coordinates and raw source-occurrence binding remain unregistered. No validated four-slot audit status is claimed.

Definition 1.1 (codeCommon).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeUniformInput.codeCommon

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeUniformInput.codeCommon (✓ std3).

Source. Repository-derived.

Commentary.

Encode the actual old literal row, finite sorted address presentation, arbitrary chronological coded history and unbounded epoch without a source value or a reachability oracle.

Definition 1.2 (materializeCells).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeUniformInput.materializeCells

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeUniformInput.materializeCells (✓ std3).

Source. Repository-derived.

Commentary.

Decode the fixed common input and return the exact required depth, original numeric class names and complete list of coded native pattern families. Malformed row or reply codes return none.

Theorem 1.3 (uniform common codec).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeUniformInput.uniform_common_codec

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

Source. Repository-derived.

Commentary.

There is one primitive recursive parseCommon. For every C,Q,H,N it round-trips codeCommon to C, sorted Q, H and N. This computational supplier is consumed by uniform_cell_materializer.

Theorem 1.4 (uniform cell materializer).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeUniformInput.uniform_cell_materializer

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

Source. Repository-derived.

Commentary.

There is one primitive recursive materializeCells. For every common input it returns exactly requiredDepth Q H, classList C mapped to original labels, and allPatterns C at that depth mapped through familyWord. Structural row-name folding, duplicate elimination, numeric sorting and exact dependent family enumeration lie on the proof path. The variable-cell materializer consumes this result.

References