The original all-menu native trajectory kernel
Abstract
The original all-menu native trajectory kernel
Source is FreeMagma Bool. Alpha is of(true), beta is of(false), and mul is an actual ordered pair. Substitution sends alpha to beta and beta to the pair (beta,alpha), extending homomorphically to every finite source. Addresses are finite Boolean lists with false=L and true=R. Readout has exactly four replies: alpha, beta, branch and absent.
A menu S is any finite ordered list of addresses. The original child menus keep their order and multiplicity. The original rank code uses the branch digits iL*N(SR)+iR before its leaf tags. The predicate Same(S,u,v) means equality of the actual reply at every q in S and every common natural count k, starting each side from its own one fixed source. No prefix closure, source-height bound or attained-vector premise is imposed.
For each address q, every source gives a branch by count pathCost(q)+2. For atomic sources this follows from guarded atomic navigation and the native Fibonacci pair recurrence. For an initial pair, descent at its first letter reduces to the corresponding actual child at the same count; induction on the remaining address proves the bound for arbitrary sources. Atomic navigation also excludes a branch before that bound on alpha. Thus a selected epsilon separates alpha from a pair immediately, and any selected nonempty address separates them by the earlier branch bound of the pair’s selected child.
The two leaves differ at each selected address at the common count pathCost(q)+1: alpha gives beta and beta gives branch. Beta can agree with a pair only when every selected address lies strictly below L. Epsilon separates at zero; L separates absent from a present root at zero; a right-starting address separates at the child’s branch bound. When eta(S)=false, every selected word is Lr with r nonempty. The pair recurrence gives equality of beta and pair(alpha,alpha) at every positive count, and at zero both replies are absent. For an empty menu this equality is vacuous. In particular a uniform beta/pair classification includes S=[]; eta=false alone never forces a nonempty left child menu.
Induction on an address-depth bound combines these semantic cases. For two pairs, synchronized substitution and literal child navigation identify equality of the complete trajectories with equality in both child menus. The existing finite product equivalence makes equality of the original branch ranks equivalent to equality of the two bounded digits. Alpha has its separate tag. Beta has a separate tag when eta=true, and otherwise has exactly the rank of pair(alpha,alpha). Induction in the child menus therefore proves both implications for the original numerical code.
The initial spatial statistic is defined on every finite Source u and every literal Address q. Write s(q)=pathCost(q), so s(epsilon)=0, s(Lq)=1+s(q), s(Rq)=2+s(q), and s(ar)=s(a)+s(r). Put e(alpha)=0 and e(beta)=1. At an initially present branch set (bq,cq)=(0,0); at an alpha leaf set (2,1); at a beta leaf set (1,0). At an absent target, the actual initial path reaches a unique blocking leaf a of color z and then has a nonempty suffix r, with q=ar. Set (bq,cq)=(s(r)+2-e(z),1 if r ends in R and 0 otherwise). The root is always present. These are the initial cases of the statistic, without a premise about a future observed trajectory.
The declaration ActualLeafHistoryRigidity.actual_address_geometry supplies absence exactly through a strict descendant of a reached initial leaf, uniqueness of comparable leaf prefixes, and readout and subtree composition under address concatenation. Two candidate blocking leaves are prefixes of the same q and hence comparable; the leaf-prefix clause makes their addresses and colors equal, and prefix cancellation makes their suffixes equal. For any initially nonbranch target, including a reached leaf with a=q and r=epsilon, its branch count is bq=s(q)-s(a)+2-e(z). The subtraction is exact because s(q)=s(a)+s(r). The statistic need not retain the blocking address or its identity.
For Tn=substitution iterated n times on alpha, T0=alpha, T1=beta, T(n+2)=pair(T(n+1),Tn), and substitution iterated k times on beta is T(k+1). NativeRankedEqualityCompiler.atomic_pair supplies the pair recurrence. NativeRankedNavigationCompiler.atomic_navigation supplies the exact reached residual and every parent-branch guard. The public finite_source_masses declaration in Geometry.FiniteSourceMass gives, for nonempty r, presence exactly when s(r)<=n and s(dropLast(r))+2<=n, the actual reached subtree T(n-s(r)), and its root reply. If r ends in R these inequalities reduce to n>=s(r); if it ends in L they reduce to n>=s(r)+1. Thus an R-ending r is absent before s(r), alpha at s(r), beta at s(r)+1, and branch thereafter. An L-ending r is absent through s(r), beta at s(r)+1, and branch thereafter. At epsilon the replies are alpha, beta, branch at counts 0,1,at least 2. In particular a final L never receives a spurious alpha phase from a zero formal residual.
NativeDepthPatterns.original_present_transport transports only an actually present initial subtree. An initial branch remains a branch by homomorphic substitution. An initial leaf at a becomes Tk or T(k+1) there according to its color. For an initially absent q=ar, transport is applied at the reached leaf a, yielding T(k+e(z)); address composition then reduces the reply at q to the guarded reply at r. No transport is applied at an absent initial literal. Substituting these indices and the initial cases above gives, for every u,q and natural k, readout(q,substitution^k(u))=branch if k>=bq; otherwise beta if bq>=1 and k=bq-1; otherwise alpha if cq=1 and k=bq-2; otherwise absent. This is an ordered case distinction with its natural-subtraction guards intact. On attained inputs cq is 0 or 1, and cq=1 implies bq>=2, so the alpha count is nonnegative and distinct from the beta and branch phases.
Consequently bq is exactly the first branch count, beta occurs exactly at bq-1 when bq>=1, and alpha occurs exactly at bq-2 when cq=1. The existing FiniteMenu.Kernel.branch_after bound gives bq<=s(q)+2 for every finite source, without a source-height restriction. atomic_branch_after and atomic_not_branch_before give the matching atomic first-branch count. Initially absent R-ending targets have bq>=3, and initially absent L-ending targets have bq>=2. In particular bq=2 can describe an initial alpha with cq=1 or initial absence with cq=0; the two cases must remain distinct.
For a fixed q define rq(u)=readout(q,u) and Kq(u)=(rq(u),bq(u)). On attained inputs cq=1 precisely when the initial reply is alpha, or it is absent and q ends in R. Conversely the initial reply is branch when bq=0, beta when bq=1, alpha when (bq,cq)=(2,1), and absent in the remaining attained cases. Hence Kq and (bq,cq) have the same equality classes. Equality of the whole future recovers the first branch count and the initial reply, and therefore the flag. The ordered phase formula reconstructs the whole future from (bq,cq). For every actual u,v, equality of their attained signatures is thus equivalent to equality of their replies at all natural counts.
The explicit separator is conditional. If the initial replies of u and v at q differ, use k=0. If those replies agree but the signatures differ, their branch counts must differ by the Kq equivalence; use k=min(bq(u),bq(v)). Exactly one reply is branch at that common count. There is no missed case of equal initial replies and equal branch counts with different attained flags. This conditional choice does not assert that arbitrary coordinate signatures can be realized independently.
For any finite ordered menu S define SigmaS(u) as the list of the initial pairs (bq,cq), in the menu’s given order, and HS(u)(k)=future(S,u,k), the ordered four-valued reply vector at one common k. List equality applies the single-address equivalence coordinate by coordinate: SigmaS(u)=SigmaS(v) if and only if HS(u)(k)=HS(v)(k) for every natural k. The two sides each use one fixed actual source throughout. S may be empty, repeated, nested, mixed, contain epsilon or omit prefixes. Repeated requests at a given count have the same required reply; this semantic equality assigns no acquisition or repeated-observation cost.
For the original bounded initial family fix D>=1 and Family(D,t): there exists a finite v with height(v)<=D and t=outer(v)=pair(alpha,v). Leaves have height zero and a pair has height one plus the maximum child height, so this is exactly height(outer(v))<=D+1. This is an initial-only family; closure under substitution is not assumed. Every legal public target p begins with R and has 1<=length(p)<=D. Writing p=Rq removes one literal first edge and yields a relative q with length(q)<D. For a public ordered list P, let S be the corresponding list of relative words; equivalently P=publicMenu(S). Order and repetitions are preserved. Every finite public subset is included by choosing an enumeration.
Define HP=max({0} union {s(p):p in P}) and B(S)=max({0} union {s(q)+2:q in S}). Since s(Rq)=s(q)+2, HP=B(S), with B(empty)=HP=0. At an outer source, the actual reply at Rq at every count is the reply at q in the same v, by present-subtree transport or homomorphism. Thus b(Rq)(outer(v))=bq(v)<=s(q)+2=s(Rq), and every selected reply is branch for every k>=HP, including counts past the initial height bound. The existing path_bounds estimate s(q)<=2*length(q) gives HP<=2D. The tail from HP is the same fixed branch vector for all members, so equality of SigmaP, equality of complete future vectors, and agreement at every common 0<=k<HP are equivalent. Unequal future vectors therefore have a single common legal separating count below HP.
One common sharpness source is t0=outer(alpha)=pair(alpha,alpha), which belongs to Family(D) for every D>=1. For every relative q, including epsilon, b(Rq)(t0)=s(q)+2 and the reply at count s(q)+1 is beta. If P is nonempty choose a target of maximal weight: its reply on this same t0 at HP-1 is beta. More generally any proposed K<HP leaves a maximal-weight target nonbranch, so HP is the least count at which all selected replies are branch uniformly on the original family. This is sharpness of HP for the selected menu. It does not say HP=2D for every menu. For the full legal menu, R repeated D times is selected, has cost 2D, and attains that upper bound; hence HP=2D, including D=1 where the relative menu contains epsilon. An empty menu has the unique empty statistic and unique empty trajectory with horizon zero.
The exported-code interface fixes public D and P before the authentic count is supplied. An encoder may use an actually acquired initial tree or actually acquired sufficient data to export an effective E(t) with finite attained alphabet. At handoff every accessible source-dependent field, including selectors, sample identities, operands, pointers, allocation distinctions, latches, transcripts, prior outputs and control, is a fixed function of E(t) and public D,P. The later decoder receives only E(t),D,P and an authentic k identifying the same-root, same-register continuation substitution^k(t), with no new Read or clock. Correctness is uniform over every original t in Family(D) and every such natural k. Acquisition, local work, installation, temporary storage, clearing and export keep their separate costs; a semantic function of t grants no free source-aware table. Unknown menus, unknown-lag acquisition, complete rows, hidden equality, full-source recovery and physical time remain separate targets.
This application combines the cited geometry, transport, guarded atomic and kernel declarations. The atomic presence and reply table use Geometry.FiniteSourceMass together with its imports. The conclusion classifies native mathematical responses and their finite temporal all-branch horizon. An encoder would still need to acquire and export sufficient source information before receiving its supplied count; these equations do not grant free access to a source-dependent code. Acquisition, retained alphabet or resource optima, controller-query horizons, physical realization and formal computability are separate questions.
Theorem 1.1 (Exact original code kernel for every menu and source).
Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/FiniteMenu/Kernel.original_menu_kernel (✓ std3). ∎
Source. Repository-derived.
Commentary.
Empty menus, epsilon, repeated targets, nested targets, mixed sides, asymmetric child menus and missing prefixes all remain included. Both sources and the count have their original unrestricted domains. This result is the trajectory-kernel clause of the finite-menu normal form; it asserts no alphabet, memory, computational or acquisition optimum.
A fixed menu’s equivalence need not survive an arbitrary tree context. With S=[LL], beta and pair(alpha,alpha) have the same selected trajectory. Placing each as the left child of a pair whose right child is alpha exposes absent versus alpha at LL at count zero. This contextual separation is compatible with the stated kernel because the context changes the sources observed by the fixed menu.