NativeUniformMaterializer
Abstract
NativeUniformMaterializer
The complete analysis is computed on a fixed first-order, infinite type of finite input codes. Primitive syntax, tree, history, ordering and budget operations are composed with the existing computable native solver. The exact theorem concerns the original native definitions for all rows, cuts, histories and epochs. Malformed codes return none; contradictory histories remain computational inputs. The complete four-way service criterion and joint online-controller evaluator remain separate obligations.
Theorem 1.1 (uniform_native_materializer).
Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeUniformMaterializer.uniform_native_materializer
Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/NativeUniformMaterializer.uniform_native_materializer (✓ std3). ∎
Source. Repository-derived.
Commentary.
One computable map is quantified before all literal rows C, cut sets Q, finite histories H and epochs N. On codeCommon C Q H N it returns the exact nativeAnalysisCode C Q H, including all raw cells, pair branches, ordered ground bindings, native summary and original K0. Every old disequality is checked under the fully composed native action. The epoch N has no effect on the returned reference bundle. This closes uniform effectiveness of native analysis and K0; it does not establish the four whole-service equivalences or online controller effectiveness.