Native Class Root Images

Abstract

Exact image filling and the finite class-root chart on complete native fibers.

Trees are all nonempty finite ordered Boolean trees. Alpha is the true leaf and beta the false leaf. The original substitution rho sends alpha to beta and beta to pair(beta,alpha), and preserves ordered pairing. A literal row C retains the concrete exterior and all occurrences of shared class names. D=Classes(C) is the finite subtype of appearing Nat labels; raw label gaps and unused Nat labels add no classes.

Theorem 1.1 (Exact Literal Leaf Evaluation).

$$\forall C:LiteralRow,(\forall f:\mathrm{Valuation}\left(Nat,Source\right),(\forall b:Bool,((\mathrm{evaluateRow}\left(f,C\right)=\mathrm{of}\left(b\right))⟺(\mathrm{lit}\left(\mathrm{RootTypeCompose}\left(f\right),b,C\right)))))$$

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

Source. Repository-derived.

Commentary.

For every exterior C, arbitrary valuation f and Boolean leaf b, evaluating C yields exactly b if and only if C is a literal b under the roots of f. The full predecessor factorization uses this criterion at visible sibling roots.

Theorem 1.2 (Roots of Extended Valuations).

$$\forall C:LiteralRow,(\forall v:\mathrm{Valuation}\left(\mathrm{Classes}\left(C\right),Source\right),(\mathrm{RootExtend}\left(C,v\right)=\mathrm{typeExtend}\left(C,\mathrm{types}\left(C,v\right)\right)))$$

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

Source. Repository-derived.

Commentary.

RootExtend(C,v) abbreviates the function n to rootType(extend(C,v,n)). Its equality with typeExtend(C,types(C,v)) holds on all natural labels, including the off-support alpha default. This identity connects literal evaluation to the finite root assignment.

Definition 1.3 (Three Reached Root Types).

$$\forall z:Source,(\mathrm{rootType}\left(z\right)=\mathrm{leafLabel}\left(z,empty\right))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.rootType (✓ std3).

Source. Repository-derived.

Commentary.

Root types are some(true)=alpha, some(false)=beta and none=branch. The empty address is always reached, so there is no absent type.

Definition 1.4 (Actual Substitution Image).

$$\forall z:Source,((\mathrm{Image}\left(z\right))⟺(\exists u:Source,(\mathrm{rho}\left(u\right)=z)))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.Image (✓ std3).

Source. Repository-derived.

Commentary.

Image membership requires an actual finite predecessor under the original substitution rho.

Definition 1.5 (Literal Leaf Predicate).

$$\forall theta:Nat\to \mathrm{Option}\left(Bool\right),(\forall b:Bool,((\forall c:Bool,((\mathrm{lit}\left(theta,b,\mathrm{leaf}\left(c\right)\right))⟺(c=b)))\wedge (\forall n:Nat,((\mathrm{lit}\left(theta,b,\mathrm{hole}\left(n\right)\right))⟺(\mathrm{theta}\left(n\right)=\mathrm{some}\left(b\right))))\wedge (\forall e:LiteralRow,(\forall g:LiteralRow,(\neg (\mathrm{lit}\left(theta,b,\mathrm{pair}\left(e,g\right)\right)))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.lit (✓ std3).

Source. Repository-derived.

Commentary.

A visible pair is never a literal leaf. A class name is a literal leaf exactly when its shared root type is that leaf.

Definition 1.6 (Finite Recursive Image Predicate).

$$\forall theta:Nat\to \mathrm{Option}\left(Bool\right),((\neg (\mathrm{im}\left(theta,alpha\right)))\wedge (\mathrm{im}\left(theta,beta\right))\wedge (\forall n:Nat,((\mathrm{im}\left(theta,\mathrm{hole}\left(n\right)\right))⟺(\neg (\mathrm{theta}\left(n\right)=alphaType))))\wedge (\forall e:LiteralRow,(\forall g:LiteralRow,((\mathrm{im}\left(theta,\mathrm{pair}\left(e,g\right)\right))⟺(((\mathrm{lit}\left(theta,false,e\right))\wedge (\mathrm{lit}\left(theta,true,g\right)))\vee ((\mathrm{im}\left(theta,e\right))\wedge (\mathrm{im}\left(theta,g\right))))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.im (✓ std3).

Source. Repository-derived.

Commentary.

AlphaType means some(true). The first pair disjunct is exactly E=pair(beta,alpha); the second is a pair of images. This is the complete NBP.10.4 recursion.

Definition 1.7 (Actual Branch Image Obligations).

$$\forall C:LiteralRow,(\forall f:Nat\to Source,((\mathrm{BranchImages}\left(C,f\right))⟺(\forall n:Nat,((\mathrm{member}\left(n,\mathrm{labels}\left(C\right)\right))⟹((\mathrm{rootType}\left(f\left(n\right)\right)=none)⟹(\mathrm{Image}\left(f\left(n\right)\right)))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.BranchImages (✓ std3).

Source. Repository-derived.

Commentary.

Only appearing branch-valued classes require actual image membership. An alpha-valued class is allowed in the right child of E.

Theorem 1.8 (Exact Test for Every Actual Filling).

$$\forall C:LiteralRow,(\forall f:Nat\to Source,((\mathrm{Image}\left(\mathrm{evaluateRow}\left(f,C\right)\right))⟺((\mathrm{BranchImages}\left(C,f\right))\wedge (\mathrm{im}\left(\mathrm{rootTypeCompose}\left(f\right),C\right)))))$$

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

Source. Repository-derived.

Commentary.

RootTypeCompose(f) maps n to rootType(f(n)). Structural induction proves the test for every literal row and every actual valuation. In the exceptional pair case both evaluated children are leaves, so their branch obligations are vacuous. For any legal x on D, put f=extend(C,x); the displayed statement becomes exactly NBP.10.6. A feasible branch type at a root hole does not make pair(alpha,alpha) an image: actual branch membership is required.

Definition 1.9 (Type Assignment on Appearing Labels).

$$\forall C:LiteralRow,(\forall theta:\mathrm{Classes}\left(C\right)\to \mathrm{Option}\left(Bool\right),(\forall n:Nat,(((\mathrm{member}\left(n,\mathrm{labels}\left(C\right)\right))⟹(\mathrm{typeExtend}\left(C,theta,n\right)=\mathrm{theta}\left(n\right)))\wedge ((\neg (\mathrm{member}\left(n,\mathrm{labels}\left(C\right)\right)))⟹(\mathrm{typeExtend}\left(C,theta,n\right)=alphaType)))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.typeExtend (✓ std3).

Source. Repository-derived.

Commentary.

On the appearing support n denotes its subtype element. Off-support defaults never create extra classes.

Definition 1.10 (Roots of Class Values).

$$\forall C:LiteralRow,(\forall x:\mathrm{Classes}\left(C\right)\to Source,(\forall d:\mathrm{Classes}\left(C\right),(\mathrm{types}\left(C,x,d\right)=\mathrm{rootType}\left(x\left(d\right)\right))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.types (✓ std3).

Source. Repository-derived.

Commentary.

The map records the root of every actual appearing class value, with the same value at all repeated occurrences.

Definition 1.11 (Exact Finite Feasible Chart).

$$\forall C:LiteralRow,(\forall theta:\mathrm{Classes}\left(C\right)\to \mathrm{Option}\left(Bool\right),((\mathrm{Admissible}\left(C,theta\right))⟺((\mathrm{im}\left(\mathrm{typeExtend}\left(C,theta\right),C\right))\wedge (\mathrm{card}\left(\mathrm{leafClasses}\left(theta,true\right)\right)\le 1)\wedge (\mathrm{card}\left(\mathrm{leafClasses}\left(theta,false\right)\right)\le 1))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.Admissible (✓ std3).

Source. Repository-derived.

Commentary.

LeafClasses(theta,b) is the subset of D with theta(d)=some(b). The bounds count distinct classes, not occurrences. Admissible is precisely membership in Theta of NBP.10.5.

Definition 1.12 (Full Actual One-Image Fiber).

$$\forall P:CutSet,(\forall C:LiteralRow,(\mathrm{OriginFiber}\left(P,C\right)=\{u:Source\Vert \mathrm{canonicalRow}\left(P,\mathrm{rho}\left(u\right)\right)=C\}))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.OriginFiber (✓ std3).

Source. Repository-derived.

Commentary.

This is U in NBP.10.2. In the realization theorem C is an actual complete canonical row. Every concrete exterior constructor, repeated occurrence, distinct-class disequality and absent-cut strict-prefix blocking leaf remains. Empty and root cuts, blocked members, zero classes and all finite source sizes are included, without rank or history bounds.

Definition 1.13 (Legal Image Fillings).

$$\forall C:LiteralRow,(\mathrm{ImageValues}\left(C\right)=\{x:\mathrm{LegalValues}\left(C\right)\Vert \mathrm{Image}\left(\mathrm{evaluateRow}\left(\mathrm{extend}\left(C,x\right),C\right)\right)\})$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.ImageValues (✓ std3).

Source. Repository-derived.

Commentary.

This is X in NBP.10.1: all injective valuations on D whose filled complete exterior is an actual image.

Definition 1.14 (Exact Image-Valuation and Origin Bijection).

$$\forall P:CutSet,((\mathrm{CutPrefixFree}\left(P\right))⟹(\forall t0:Source,(\mathrm{Equiv}\left(\mathrm{ImageValues}\left(\mathrm{canonicalRow}\left(P,t0\right)\right),\mathrm{OriginFiber}\left(P,\mathrm{canonicalRow}\left(P,t0\right)\right)\right))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.imageOriginEquiv (✓ std3).

Source. Repository-derived.

Commentary.

The forward map is x to delta(evaluateRow(extend(C,x),C)), where delta is the original unique inverse on rho[Source]. The inverse recovers the class subtrees of rho(u) using their canonical representatives. The exact legal-row equivalence and both inverse laws give the NBP.10.3 bijection.

Theorem 1.15 (Exact Types Attained Throughout the Actual Fiber).

$$\forall P:CutSet,((\mathrm{CutPrefixFree}\left(P\right))⟹(\forall t0:Source,(\forall theta:\mathrm{Classes}\left(\mathrm{canonicalRow}\left(P,t0\right)\right)\to \mathrm{Option}\left(Bool\right),((\mathrm{Admissible}\left(\mathrm{canonicalRow}\left(P,t0\right),theta\right))⟺(\exists u:\mathrm{OriginFiber}\left(P,\mathrm{canonicalRow}\left(P,t0\right)\right),(\mathrm{types}\left(\mathrm{canonicalRow}\left(P,t0\right),\mathrm{recover}\left(P,\mathrm{rho}\left(u\right)\right)\right)=theta))))))$$

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

Source. Repository-derived.

Commentary.

Recover(P,rho(u)) abbreviates the legal valuation recovered in the complete row C=canonicalRow(P,t0), with the prefix-free proof supplied. This is exact NBP.10.7 on the entire actual NBP.10.2 domain. Enumerate the finite subtype D through e:D equivalent to Fin(card D). Leaf classes receive their forced leaves. Branch class d receives rho(pair(code(card D,e(d)),alpha)); these are images with branch roots, pairwise distinct by code and substitution injectivity, and distinct from both leaves. The cardinality bounds give full injectivity, and the recursive test gives image membership. The image-origin bijection realizes the assignment. Conversely, any origin recovers an injective image valuation; injectivity allows at most one class at each leaf. The construction includes zero branch classes and zero classes.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.Admissible
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.BranchImages
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.Image
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.ImageValues
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.OriginFiber
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.class_root_chart
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.evaluate_leaf
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.filling_image_iff
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.im
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.imageOriginEquiv
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.lit
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.rootType
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.root_extend
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.typeExtend
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage.types
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/NativeCutFibers
• Dependency: D5/S3/Arith/FibonacciAtomic/SourceCoordinates/IntrinsicSubstitutionCoordinates