Native Class Root Padding

Abstract

Finite image padding realizes every feasible class-root assignment with exact bounded native replies.

Sources are all finite nonempty ordered Boolean trees. The substitution rho sends alpha to beta, sends beta to pair(beta,alpha), and preserves pairing. For a prefix-free finite cut P and a source t0, write C=canonicalRow(P,t0). Its occurring class set D=Classes(C) identifies repeated holes. ImageValues(C) consists of injective class valuations whose complete filling is an actual rho image; OriginFiber(P,C) consists of all finite origins with complete current row C. No source-size bound is imposed.

Definition 1.1 (Reached Constructor Reply).

$$(\mathrm{rootReply}\left(\mathrm{some}\left(true\right)\right)=alpha)\wedge (\mathrm{rootReply}\left(\mathrm{some}\left(false\right)\right)=beta)\wedge (\mathrm{rootReply}\left(none\right)=branch)$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootPadding.rootReply (✓ std3).

Source. Repository-derived.

Commentary.

The three root types some(true), some(false), and none mean alpha, beta, and branch respectively. An actual class root is reached, so it has no absent type.

Definition 1.2 (Exterior and First-Class Query Rule).

$$\forall theta:Nat\to \mathrm{Option}\left(Bool\right),((\forall a:Address,(\forall b:Bool,(\mathrm{queryReply}\left(theta,a,\mathrm{leaf}\left(b\right)\right)=\mathrm{readout}\left(a,\mathrm{leaf}\left(b\right)\right))))\wedge (\forall d:Nat,(\mathrm{queryReply}\left(theta,empty,\mathrm{hole}\left(d\right)\right)=\mathrm{rootReply}\left(\mathrm{theta}\left(d\right)\right)))\wedge (\forall d:Nat,(\forall a:Address,((\neg (a=empty))⟹(((\mathrm{theta}\left(d\right)=none)⟹(\mathrm{queryReply}\left(theta,a,\mathrm{hole}\left(d\right)\right)=branch))\wedge ((\neg (\mathrm{theta}\left(d\right)=none))⟹(\mathrm{queryReply}\left(theta,a,\mathrm{hole}\left(d\right)\right)=absent))))))\wedge (\forall l:LiteralRow,(\forall r:LiteralRow,((\mathrm{queryReply}\left(theta,empty,\mathrm{pair}\left(l,r\right)\right)=branch)\wedge (\forall a:Address,((\mathrm{queryReply}\left(theta,\mathrm{left}\left(a\right),\mathrm{pair}\left(l,r\right)\right)=\mathrm{queryReply}\left(theta,a,l\right))\wedge (\mathrm{queryReply}\left(theta,\mathrm{right}\left(a\right),\mathrm{pair}\left(l,r\right)\right)=\mathrm{queryReply}\left(theta,a,r\right))))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootPadding.queryReply (✓ std3).

Source. Repository-derived.

Commentary.

Follow the fixed exterior until a concrete reply or a class hole is encountered. Only that one class type is inspected. An empty suffix returns its constructor. A nonempty suffix returns absent for either leaf type and branch for a branch type. Thus concrete blocking leaves, absent addresses, root holes and repeated-class occurrences are included.

Definition 1.3 (Inclusive Branch Depth).

$$\forall C:LiteralRow,(\forall L:Nat,(\forall v:\mathrm{Classes}\left(C\right)\to Source,((\mathrm{DeepValues}\left(C,L,v\right))⟺(\forall d:\mathrm{Classes}\left(C\right),((\mathrm{rootType}\left(v\left(d\right)\right)=none)⟹(\forall a:Address,((\mathrm{length}\left(a\right)\le L)⟹(\mathrm{readout}\left(a,v\left(d\right)\right)=branch))))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootPadding.DeepValues (✓ std3).

Source. Repository-derived.

Commentary.

Every address of length at most L inside a branch-valued class returns branch. In particular no such class has a leaf at depth at most L; its minimum native leaf depth is strictly greater than L.

Theorem 1.4 (Simultaneous Actual Padding and Query Correspondence).

$$\forall P:CutSet,((\mathrm{CutPrefixFree}\left(P\right))⟹(\forall t0:Source,(\forall L:Nat,(\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 v:\mathrm{ImageValues}\left(\mathrm{canonicalRow}\left(P,t0\right)\right),(\exists u:\mathrm{OriginFiber}\left(P,\mathrm{canonicalRow}\left(P,t0\right)\right),((\mathrm{rho}\left(u\right)=\mathrm{evaluateRow}\left(\mathrm{extend}\left(\mathrm{canonicalRow}\left(P,t0\right),v\right),\mathrm{canonicalRow}\left(P,t0\right)\right))\wedge (\mathrm{types}\left(\mathrm{canonicalRow}\left(P,t0\right),v\right)=theta)\wedge (\mathrm{DeepValues}\left(\mathrm{canonicalRow}\left(P,t0\right),L,v\right))\wedge (\forall a:Address,((\mathrm{length}\left(a\right)\le L)⟹(\mathrm{readout}\left(a,\mathrm{rho}\left(u\right)\right)=\mathrm{queryReply}\left(\mathrm{typeExtend}\left(\mathrm{canonicalRow}\left(P,t0\right),theta\right),a,\mathrm{canonicalRow}\left(P,t0\right)\right))))))))))))$$

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

Source. Repository-derived.

Commentary.

For each admissible assignment theta, one finite valuation and one actual origin satisfy all displayed conclusions together. Different classes remain distinct and every repeated occurrence uses its class value. Branch classes receive distinct image codes duplicated into complete binary trees of depth L+1. Duplication preserves injectivity and image membership; induction on addresses proves the branch-depth bound. Leaf classes receive their forced literals, whose multiplicity bounds ensure injectivity across the entire valuation. The exact image grammar and legal-row theorem give the original finite origin. Structural induction through the exterior then gives every bounded native reply on this same image. Choosing these valuations for all admissible theta gives the simultaneous family, including zero classes and zero branch classes. No cross-origin distinction is required. The chosen finite origins are representatives, not a reconstruction of every source. The result supplies no acquisition permission, runtime query extraction, physical operation or controller-state bound.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootPadding.DeepValues
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootPadding.padded_native_query_chart
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootPadding.queryReply
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootPadding.rootReply
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage