Native Class Root Simulation

Abstract

Finite native dialogues compile to legal class-root experiments on truthful fixed actual representatives.

Sources are finite ordered Boolean trees and rho is the original substitution. For a finite prefix-free cut P and source T, let C=canonicalRow(P,T). ImageValues(C) contains every injective class valuation whose filled complete row is an actual image; OriginFiber(P,C) contains every finite origin with complete current row C. Types take the values some(true), some(false), and none for alpha, beta, and branch. Chart(C) is the set of admissible assignments. Dialogue is the existing finite four-reply native reader tree with complete row outputs. The notation replies(t) means the function a ↦ readout(a,t); valuations and origins are coerced to their underlying values in formulas.

Definition 1.1 (Legal Three-Reply Experiment Trees).

$$\forall C:LiteralRow,(\forall O:Type,((\mathrm{stop}\left(\right):O\to \mathrm{RootTree}\left(C,O\right))\wedge (\mathrm{ask}\left(\right):\mathrm{Classes}\left(C\right)\to \mathrm{RootTree}\left(C,O\right)\to \mathrm{RootTree}\left(C,O\right)\to \mathrm{RootTree}\left(C,O\right)\to \mathrm{RootTree}\left(C,O\right))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootSimulation.RootTree (✓ std3).

Source. Repository-derived.

Commentary.

A root tree has a complete output at a stop and exactly three continuations at a query of an appearing class. There is no absent root reply and no query constructor when the class set is empty.

Definition 1.2 (Stationary Native Execution).

$$\forall O:Type,(\forall f:Address\to Reply,((\forall o:O,(\mathrm{nativeRun}\left(f,\mathrm{stop}\left(o\right)\right)=(o,0)))\wedge (\forall a:Address,(\forall A:\mathrm{Dialogue}\left(O\right),(\forall B:\mathrm{Dialogue}\left(O\right),(\forall E:\mathrm{Dialogue}\left(O\right),(\forall D:\mathrm{Dialogue}\left(O\right),(\mathrm{nativeRun}\left(f,\mathrm{read}\left(a,A,B,E,D\right)\right)=\mathrm{increment}\left(\mathrm{nativeRun}\left(f,\mathrm{choose}\left(f\left(a\right),A,B,E,D\right)\right)\right)))))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootSimulation.nativeRun (✓ std3).

Source. Repository-derived.

Commentary.

Execution follows the actual alpha, beta, branch, or absent continuation. The pair records the terminal output and invocation count; increment(o,n)=(o,n+1). The register reply function stays fixed; every visited read counts once, including repeats and absences.

Definition 1.3 (Joint Root Execution).

$$\forall C:LiteralRow,(\forall O:Type,(\forall theta:\mathrm{Classes}\left(C\right)\to \mathrm{Option}\left(Bool\right),((\forall o:O,(\mathrm{rootRun}\left(theta,\mathrm{stop}\left(o\right)\right)=(o,0)))\wedge (\forall d:\mathrm{Classes}\left(C\right),(\forall A:\mathrm{RootTree}\left(C,O\right),(\forall B:\mathrm{RootTree}\left(C,O\right),(\forall E:\mathrm{RootTree}\left(C,O\right),(\mathrm{rootRun}\left(theta,\mathrm{ask}\left(d,A,B,E\right)\right)=\mathrm{increment}\left(\mathrm{rootRun}\left(theta,\mathrm{chooseRoot}\left(\mathrm{theta}\left(d\right),A,B,E\right)\right)\right)))))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootSimulation.rootRun (✓ std3).

Source. Repository-derived.

Commentary.

Execution follows the same unchanged joint assignment at every vertex. The function chooseRoot selects the alpha, beta, or branch child for some(true), some(false), or none. Every visited class query counts once. Early stops use no invocation.

Definition 1.4 (Native Path Budget).

$$\forall O:Type,((\forall o:O,(\mathrm{nativeDepth}\left(\mathrm{stop}\left(o\right)\right)=0))\wedge (\forall a:Address,(\forall A:\mathrm{Dialogue}\left(O\right),(\forall B:\mathrm{Dialogue}\left(O\right),(\forall E:\mathrm{Dialogue}\left(O\right),(\forall D:\mathrm{Dialogue}\left(O\right),(\mathrm{nativeDepth}\left(\mathrm{read}\left(a,A,B,E,D\right)\right)=\max \left(\mathrm{nativeDepth}\left(A\right),\mathrm{nativeDepth}\left(B\right),\mathrm{nativeDepth}\left(E\right),\mathrm{nativeDepth}\left(D\right)\right)+1)))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootSimulation.nativeDepth (✓ std3).

Source. Repository-derived.

Commentary.

The depth is zero at a stop and one plus the maximum depth of the four children at a read.

Definition 1.5 (Experiment Path Budget).

$$\forall C:LiteralRow,(\forall O:Type,((\forall o:O,(\mathrm{rootDepth}\left(\mathrm{stop}\left(o\right)\right)=0))\wedge (\forall d:\mathrm{Classes}\left(C\right),(\forall A:\mathrm{RootTree}\left(C,O\right),(\forall B:\mathrm{RootTree}\left(C,O\right),(\forall E:\mathrm{RootTree}\left(C,O\right),(\mathrm{rootDepth}\left(\mathrm{ask}\left(d,A,B,E\right)\right)=\max \left(\mathrm{rootDepth}\left(A\right),\mathrm{rootDepth}\left(B\right),\mathrm{rootDepth}\left(E\right)\right)+1)))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootSimulation.rootDepth (✓ std3).

Source. Repository-derived.

Commentary.

The depth is zero at a stop and one plus the maximum depth of the three children at a class experiment.

Definition 1.6 (Finite Native Word Bound).

$$\forall O:Type,((\forall o:O,(\mathrm{wordBound}\left(\mathrm{stop}\left(o\right)\right)=0))\wedge (\forall a:Address,(\forall A:\mathrm{Dialogue}\left(O\right),(\forall B:\mathrm{Dialogue}\left(O\right),(\forall E:\mathrm{Dialogue}\left(O\right),(\forall D:\mathrm{Dialogue}\left(O\right),(\mathrm{wordBound}\left(\mathrm{read}\left(a,A,B,E,D\right)\right)=\max \left(\mathrm{length}\left(a\right),\mathrm{wordBound}\left(A\right),\mathrm{wordBound}\left(B\right),\mathrm{wordBound}\left(E\right),\mathrm{wordBound}\left(D\right)\right))))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootSimulation.wordBound (✓ std3).

Source. Repository-derived.

Commentary.

The maximum ranges over all installed query words, including unrealized edges. A stop contributes zero. This is a bound on this one finite comparator, not on source size.

Definition 1.7 (Exterior Navigation and Experiment Compilation).

$$\forall C:LiteralRow,(\forall O:Type,((\forall o:O,(\mathrm{compileRoot}\left(C,\mathrm{stop}\left(o\right)\right)=\mathrm{stop}\left(o\right)))\wedge (\forall a:Address,(\forall A:\mathrm{Dialogue}\left(O\right),(\forall B:\mathrm{Dialogue}\left(O\right),(\forall E:\mathrm{Dialogue}\left(O\right),(\forall D:\mathrm{Dialogue}\left(O\right),((\forall y:Reply,((\mathrm{firstClass}\left(C,a\right)=\mathrm{inl}\left(y\right))⟹(\mathrm{compileRoot}\left(C,\mathrm{read}\left(a,A,B,E,D\right)\right)=\mathrm{compileRoot}\left(C,\mathrm{choose}\left(y,A,B,E,D\right)\right))))\wedge (\forall d:\mathrm{Classes}\left(C\right),(\forall b:Bool,((\mathrm{firstClass}\left(C,a\right)=\mathrm{inr}\left((d,b)\right))⟹(\mathrm{compileRoot}\left(C,\mathrm{read}\left(a,A,B,E,D\right)\right)=\mathrm{ask}\left(d,\mathrm{compileRoot}\left(C,\mathrm{choose}\left(\mathrm{classReply}\left(b,\mathrm{some}\left(true\right)\right),A,B,E,D\right)\right),\mathrm{compileRoot}\left(C,\mathrm{choose}\left(\mathrm{classReply}\left(b,\mathrm{some}\left(false\right)\right),A,B,E,D\right)\right),\mathrm{compileRoot}\left(C,\mathrm{choose}\left(\mathrm{classReply}\left(b,none\right),A,B,E,D\right)\right)\right)))))))))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootSimulation.compileRoot (✓ std3).

Source. Repository-derived.

Commentary.

The exterior is traversed to its first class hole, if any. A fixed exterior reply selects one compiled continuation without a class experiment. A hole yields one legal appearing class d and a Boolean b recording whether the remaining suffix is nonempty. When b is false, the class constructor selects the matching native continuation. When b is true, either leaf selects absent and a branch selects branch. Repeated questions remain distinct charged vertices. The symbols firstClass, classReply and choose denote these structural operations; choose(y,A,B,E,D) selects the four-reply child.

Definition 1.8 (Exactly Attained Joint Types).

$$\forall C:LiteralRow,(\mathrm{Chart}\left(C\right)=\{theta:\mathrm{Classes}\left(C\right)\to \mathrm{Option}\left(Bool\right)\Vert \mathrm{Admissible}\left(C,theta\right)\})$$

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootSimulation.Chart (✓ std3).

Source. Repository-derived.

Commentary.

Admissibility uses the complete exterior image grammar and the separate multiplicity bounds on the two literal leaf classes. The actual class-root image theorem identifies this chart with exactly the attained types.

Theorem 1.9 (Truthful Joint Simulation on Actual Origins).

$$\forall P:CutSet,((\mathrm{CutPrefixFree}\left(P\right))⟹(\forall T:Source,(\forall S:Type,([\mathrm{Finite}\left(S\right)]\forall sigma:\mathrm{ImageValues}\left(\mathrm{canonicalRow}\left(P,T\right)\right)\to S,(\forall E:S\to \mathrm{Dialogue}\left(LiteralRow\right),(\forall q:Nat,(((\forall s:S,(\mathrm{nativeDepth}\left(E\left(s\right)\right)\le q))\wedge (\forall w:\mathrm{ImageValues}\left(\mathrm{canonicalRow}\left(P,T\right)\right),(\forall z:\mathrm{OriginFiber}\left(P,\mathrm{canonicalRow}\left(P,T\right)\right),((\mathrm{rho}\left(z\right)=\mathrm{evaluateRow}\left(\mathrm{extend}\left(\mathrm{canonicalRow}\left(P,T\right),w\right),\mathrm{canonicalRow}\left(P,T\right)\right))⟹(\mathrm{fst}\left(\mathrm{nativeRun}\left(\mathrm{replies}\left(\mathrm{rho}\left(z\right)\right),E\left(\mathrm{sigma}\left(w\right)\right)\right)\right)=\mathrm{canonicalRow}\left(P,z\right))))))⟹(\exists v:\mathrm{Chart}\left(\mathrm{canonicalRow}\left(P,T\right)\right)\to \mathrm{ImageValues}\left(\mathrm{canonicalRow}\left(P,T\right)\right),(\exists u:\mathrm{Chart}\left(\mathrm{canonicalRow}\left(P,T\right)\right)\to \mathrm{OriginFiber}\left(P,\mathrm{canonicalRow}\left(P,T\right)\right),(\exists c:\mathrm{Chart}\left(\mathrm{canonicalRow}\left(P,T\right)\right)\to S,(\forall theta:\mathrm{Chart}\left(\mathrm{canonicalRow}\left(P,T\right)\right),((\mathrm{rho}\left(u\left(theta\right)\right)=\mathrm{evaluateRow}\left(\mathrm{extend}\left(\mathrm{canonicalRow}\left(P,T\right),v\left(theta\right)\right),\mathrm{canonicalRow}\left(P,T\right)\right))\wedge (\mathrm{types}\left(\mathrm{canonicalRow}\left(P,T\right),v\left(theta\right)\right)=theta)\wedge (c\left(theta\right)=\mathrm{sigma}\left(v\left(theta\right)\right))\wedge (\mathrm{fst}\left(\mathrm{rootRun}\left(theta,\mathrm{compileRoot}\left(\mathrm{canonicalRow}\left(P,T\right),E\left(c\left(theta\right)\right)\right)\right)\right)=\mathrm{canonicalRow}\left(P,u\left(theta\right)\right))\wedge (\mathrm{snd}\left(\mathrm{rootRun}\left(theta,\mathrm{compileRoot}\left(\mathrm{canonicalRow}\left(P,T\right),E\left(c\left(theta\right)\right)\right)\right)\right)\le \mathrm{snd}\left(\mathrm{nativeRun}\left(\mathrm{replies}\left(\mathrm{rho}\left(u\left(theta\right)\right)\right),E\left(\mathrm{sigma}\left(v\left(theta\right)\right)\right)\right)\right))\wedge (\mathrm{rootDepth}\left(\mathrm{compileRoot}\left(\mathrm{canonicalRow}\left(P,T\right),E\left(c\left(theta\right)\right)\right)\right)\le q)))))))))))))$$

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

Source. Repository-derived.

Commentary.

Fix an arbitrary finite supplement alphabet S, a supplement sigma depending on the complete acquired valuation, and one finite native dialogue E(s) per value. Assume every installed dialogue has depth at most q and gives the complete predecessor row on every matching actual valuation and origin. There is one fixed actual origin u(theta), one injective image valuation v(theta), and its truthful exported value c(theta)=sigma(v(theta)) for every admissible joint type. The compiled tree returns that origin’s entire canonical predecessor row, uses no more calls than its native run, and has depth at most q. To obtain a common finite word bound, take the maximum over all installed dialogues. Apply actual image padding at that bound, then induct through each dialogue using structural exterior navigation. Each vertex is constant or depends on exactly one appearing class, so zero or one class experiment reproduces its native reply on that same padded image. The supplement alphabet is retained unchanged. No assertion says that sigma is constant on all sources of one type. The result covers arbitrary addresses, repeated calls, blocking absences, zero queries, root cuts, empty cuts and zero classes. It is the finite-dialogue simulation needed for the necessity direction of the joint feasibility correspondence. The general source-total reader unrolling, full predecessor factorization through types, reverse native implementation and complete feasibility equivalence are separate obligations. No source reconstruction chart, physical resource equivalence, acquisition permission or controller-state bound follows.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootSimulation.Chart
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootSimulation.RootTree
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootSimulation.compileRoot
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootSimulation.nativeDepth
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootSimulation.nativeRun
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootSimulation.rootDepth
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootSimulation.rootRun
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootSimulation.truthful_joint_root_simulation
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootSimulation.wordBound
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootImage
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/NativeClassRootPadding
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/NativePassiveServiceRealization