Free native states resist countable parameterization
Abstract
NativeFreeStateCardinality
Theorem 1.1 (Infinite stream trees and the complete solution domain).
Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativeFreeStateCardinality.free_state_cardinality (✓ std3). ∎
Source. Repository-derived.
Commentary.
The domain is the existing unrestricted native completion, including arbitrary infinite ordered trees. A Boolean stream s determines a tree U(s) whose left child is U(tail(s)) and whose right child is the atomic leaf for its first bit. False selects the alpha leaf and true the beta leaf. Thus this construction retains exactly the two native atoms of ranks zero and one, without introducing a new leaf label.
The address bitAddress(j) consists of j left edges followed by one right edge. The subtree there is exactly the leaf for s(j); it is reached for every natural j. The corecursor constructs one complete tree for the entire stream, and induction on j proves this whole-subtree identity. Equal completed trees therefore have equal bits at every index. Every constructed tree has actual finite leaf subtrees and differs from the entirely leafless Omega.
In the formula U denotes streamTree, tail(s)(j) is s(j+1), and not is Boolean negation. Subtree returns an optional whole tree, so some explicitly certifies presence. The final quantifier ranges over every countable parameter type A and every function decode into CompletionTree. Surjective has its ordinary function-theoretic meaning.
Injectivity supplies continuum many distinct completed native solutions of the retained equation X = X. If the completed domain were countable, encoding its elements by natural numbers and composing with this injection and characteristic functions of subsets of the naturals would contradict the existing Cantor theorem. A surjection from any countable parameter domain would make the completed domain countable, so no such surjection exists.
A finite family of branches with finitely many integer parameters in each branch has a countable disjoint union of parameter tuples. Any deterministic assignment of canonical terminals or Omega from those data is a function of that countable domain and therefore cannot enumerate all native completed solutions. This statement concerns branches determined by their data. A branch retaining an unrestricted completed free state has a different parameter domain and is not ruled out. Neither a normalization algorithm for arbitrary retained equations nor an effective elimination of free states follows.
The result is an unrestricted recursive construction and structural obstruction. It is not a bounded enumeration, a finite numerical instance, a checker or a numerical reduction. No literature-wide novelty is asserted.