Native Indexed Role Lists
Abstract
Concrete deterministic exact role lists for arbitrary indexed native read constraints.
Source is the entire set of finite nonempty ordered FreeMagma Bool terms. Alpha is of(true), beta is of(false), and pair is mul. The original substitution sends alpha to beta, beta to pair(beta,alpha), and pairs to pairs of images. Class A is exactly alpha, H is exactly beta, I is the original actual substitution image with beta removed, and O is the complement of their union. The computable kind classifier agrees with these four disjoint classes. Applying the original pair_image theorem gives type I exactly for the ordered pairs (H,A), (H,H), (H,I), (I,H), (I,I); the other eleven give O. No branch has leaf type.
Roles are in original order a,c,bone,btwo,bthree,bfour. Their native filling indices are 0,3,1,2,4,5, using the original dToNative permutation. The physical occurrences LLL and LRL share a; RLL and RRL share c; LLR, LRR, RLR and RRR give bone, btwo, bthree and bfour. These are whole subtree identities, not Boolean labels. Different role lists may overlap.
An arbitrary installed record family has literals words(i) and requested raw replies replies(i), indexed by every i in Fin(n). Install keeps the original index of every word of length at least three, its actual occurrence role, the suffix after those three letters, and its requested reply. It preserves duplicate suffixes and separate repeated-role occurrences. ShortGuard requires branch on every shorter word, including the empty word. Both conditions refer to the same proposed reply family.
Under(v,R) follows the actual prefix trie edges, removing exactly v from every surviving suffix. Its membership theorem restores v and preserves the index, role and reply. Explicit(v) means that some record survives; markers retain every ending index in its original order. RootNode describes the suffix-record trie. The original installedRoot is # exactly when n=0 and is the explicit empty-address root for every nonempty raw menu, including a menu consisting entirely of short reads. ChildNode uses # precisely when no record lies below that child. NodeRecords at # is empty. Thus # admits an arbitrary finite subtree and never denotes a missing actual child of a pair.
The function lists(R,v,d,k) contains actual Source values. At # its prescribed lists are [alpha], [beta], [B(1),…,B(6)], and [pair(alpha,B(1)),…,pair(alpha,B(6))]. Here B(j) is the original padding of beta. The original pad_preimage proves image membership, and B_height proves all six entries distinct. Each I and O list has length six; each leaf list has length one.
At an explicit root with no suffix records the construction still pairs the prescribed # child bases. At an explicit node, alpha or beta is retained exactly when every ending index of that role asks for that leaf and every strict descendant index of that role asks for absent. This test does not require either child branch language to be realizable. A pair is permitted exactly when every ending role index asks for branch. In fixed A,H,I,O order the construction considers all sixteen ordered child-type pairs, enumerates their concrete retained left and right values, assigns the original parent type, removes duplicate whole terms and keeps the first six. Other roles impose no condition.
Exact(L,K) asserts that L has no repeated values, its length is at most six, all members lie in K, and if its length is less than six every member of K occurs in L. Language(R,d,k) consists of terms of type k satisfying every indexed raw readout for d. NodeLanguage uses the rebased records at that node. OriginalLanguage instead quantifies directly over every original i and every length-three occurrence followed by v and a residual suffix. The theorem identifies these two languages for every address, including empty and contradictory fibers.
The induction budget bounds only the finite observed suffix lengths, without bounding source size, source depth or compatible-language cardinality. The resulting list is independent of any larger valid recursion budget. Consequently the public explicit-node recurrence uses exactly the lists assigned to the two actual trie children. An unconstrained child always uses the same fixed basis.
For the pair induction, an actual compatible pair provides nonempty child languages. Exactness supplies at least one retained value in each. If either retained child list is saturated, pairing its six distinct members with one retained value of the other supplies six different parents of the required type. Therefore a short parent candidate list forces both relevant child lists to be complete. Unique ordered decomposition then supplies every actual pair. A zero child language supplies no parent. This proves the invariant without subtraction, inclusion-exclusion, finite-language assumptions or classical selection of data.
In the displayed formula, toENat is the natural-number cast to extended naturals, rho is the original substitution, and Fiber is NativeSixSourceCones.Fiber. Set.encard is the extended-natural cardinality, so the length of each list equals min(6,encard(K)) also when K is infinite or empty. For a short list, soundness and completeness identify its finite set with the entire language. A saturated list gives a six-element subset of K. The cardinal equation follows in either case from the original list invariant and pinned Set.encard monotonicity.
For every arbitrary native filling x, all proposed installed readouts hold exactly when ShortGuard holds and each x(dToNative(d)) satisfies its original role constraints. The same statement holds for every original origin u in NativeSixSourceCones.Fiber: the original recover and recover_fill reconstruct its entire current image as filling(recoveredNative(u)). The root lists, selected at installedRoot(n), are exact lists for the original typed role languages C(d). This is the actual native root correspondence, with no assumed recurrence or realization bridge.
Contradictory duplicates, empty suffixes, impossible root absence, early leaves and all-absent descendant cones follow the same rules. The statement supplies no shared semantic DAG, DAG node bound, polynomial-time implementation, matching theorem or new truncation-transfer theorem. It formalizes the source-specific constructive recurrence of the native finite-table classification Lemma 4.2, using the existing image grammar, original B suppliers and mature finite-list and cardinality facts. It asserts no literature novelty.
Theorem 1.1 (All Original Native Role Languages).
Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/FiniteMenu/NativeIndexedRoleLists.native_indexed_role_lists (✓ std3). ∎
Source. Repository-derived.
Commentary.
Specification includes the four original classes, the prescribed # basis and the empty-record explicit-root rule, exactness and extended-natural cardinality at every node, exact leaf and branch rules, prefix and marker correspondence, actual root and child records, the explicit recurrence, every original indexed language, exact original root lists and their cardinality, arbitrary native filling equivalence, and the recovered-origin root equivalence. Every field has its full universal quantifiers; no finite compatible-language premise is imposed.