Chronological Child Prefixes for Residue Protocols

Abstract

Every identifying residue protocol has chronological child prefixes; every ordered identifying child family with internal nonlast heads has an exact parent realization.

Let p be prime, let d<e be natural numbers, and let b be a residue modulo p to the power d. The nonempty finite set I consists of next-depth labels over b. Write k=card(I), X=ZMod(p^e), C(z) for the complete fiber of z at depth d+1, and S for the union of C(z) over z in I. These are the node, children and siblings fibers of residue geometry. Labels and members of I are coerced to their underlying residues.

Tree denotes PassiveProtocol X with natural-number answers. The actual readout q(c,a) is the greatest congruence depth of c and a, including zero and e. R(T,a) is runPassiveProtocol q T a, a list of Sigma records containing each center and its actual answer. Write Trace for this list type, entry(c,r) for one record, len for list length, app for concatenation and one for a singleton list. Ident(A,T) means that R(T,a)=R(T,b) for a,b in A implies a=b. Equiv(A,B) denotes bijections and Map(A,B) denotes functions. No bound on the number of syntactic nodes or on the depths of all answer branches is assumed.

Theorem 1.1 (Extraction and arbitrary-family realization).

$$\forall p,e,d\in \mathbb{N},\left(\left(\mathrm{Prime}\left(p\right)\right)\wedge \left(d<e\right)\right)\Rightarrow \left(\forall b\in \mathrm{ZMod}\left(\mathrm{pow}\left(p,d\right)\right),\forall I\in \mathrm{Finset}\left(\mathrm{ZMod}\left(\mathrm{pow}\left(p,d+1\right)\right)\right),\left(\left(\mathrm{Nonempty}\left(I\right)\right)\wedge \left(\mathrm{Subset}\left(I,\mathrm{children}\left(p,d,b\right)\right)\right)\right)\Rightarrow \left(\left(\forall T\in Tree,\left(\mathrm{Ident}\left(S,T\right)\right)\Rightarrow \left(\exists o\in \mathrm{Equiv}\left(\mathrm{Fin}\left(k\right),I\right),\exists U\in \mathrm{Map}\left(\mathrm{Fin}\left(k\right),Tree\right),\exists P\in \mathrm{Map}\left(\mathrm{Fin}\left(k\right),Trace\right),\exists c\in \mathrm{Map}\left(\mathrm{Fin}\left(k\right),X\right),\exists next\in \mathrm{Map}\left(\mathrm{Fin}\left(k\right),\mathrm{Map}\left(\mathbb{N},Tree\right)\right),\left[\begin{array}{r}\left(\forall i\in \mathrm{Fin}\left(k\right),\left[\begin{array}{r}\left(\mathrm{apply}\left(c,i\right)\in C\left(\mathrm{apply}\left(o,i\right)\right)\right)\\ \wedge \left(\mathrm{Ident}\left(C\left(\mathrm{apply}\left(o,i\right)\right),\mathrm{apply}\left(U,i\right)\right)\right)\\ \wedge \left(\left(\left(i+1<k\right)\vee \left(\left(k=1\right)\wedge \left(d+1<e\right)\right)\right)\Rightarrow \left(\mathrm{apply}\left(U,i\right)=\mathrm{query}\left(\mathrm{apply}\left(c,i\right),\mathrm{apply}\left(next,i\right)\right)\right)\right)\\ \wedge \left(i\le \mathrm{len}\left(\mathrm{apply}\left(P,i\right)\right)\right)\\ \wedge \left(\forall a\in C\left(\mathrm{apply}\left(o,i\right)\right),R\left(T,a\right)=\mathrm{app}\left(\mathrm{apply}\left(P,i\right),R\left(\mathrm{apply}\left(U,i\right),a\right)\right)\right)\end{array}\right]\right)\\ \wedge \left(\forall i\in \mathrm{Fin}\left(k\right),\forall j\in \mathrm{Fin}\left(k\right),\left(i<j\right)\Rightarrow \left(\mathrm{IsPrefix}\left(\mathrm{app}\left(\mathrm{apply}\left(P,i\right),\mathrm{one}\left(\mathrm{entry}\left(\mathrm{apply}\left(c,i\right),d\right)\right)\right),\mathrm{apply}\left(P,j\right)\right)\right)\right)\end{array}\right]\right)\right)\wedge \left(\forall o\in \mathrm{Equiv}\left(\mathrm{Fin}\left(k\right),I\right),\forall U\in \mathrm{Map}\left(\mathrm{Fin}\left(k\right),Tree\right),\left(\left(\forall i\in \mathrm{Fin}\left(k\right),\mathrm{Ident}\left(C\left(\mathrm{apply}\left(o,i\right)\right),\mathrm{apply}\left(U,i\right)\right)\right)\wedge \left(\forall i\in \mathrm{Fin}\left(k\right),\left(i+1<k\right)\Rightarrow \left(\exists x\in C\left(\mathrm{apply}\left(o,i\right)\right),\exists f\in \mathrm{Map}\left(\mathbb{N},Tree\right),\mathrm{apply}\left(U,i\right)=\mathrm{query}\left(x,f\right)\right)\right)\right)\Rightarrow \left(\exists c\in \mathrm{Map}\left(\mathrm{Fin}\left(k\right),X\right),\exists next\in \mathrm{Map}\left(\mathrm{Fin}\left(k\right),\mathrm{Map}\left(\mathbb{N},Tree\right)\right),\exists V\in Tree,\left[\begin{array}{r}\left(\forall i\in \mathrm{Fin}\left(k\right),\left(i+1<k\right)\Rightarrow \left(\left(\mathrm{apply}\left(c,i\right)\in C\left(\mathrm{apply}\left(o,i\right)\right)\right)\wedge \left(\mathrm{apply}\left(U,i\right)=\mathrm{query}\left(\mathrm{apply}\left(c,i\right),\mathrm{apply}\left(next,i\right)\right)\right)\right)\right)\\ \wedge \left(\mathrm{Ident}\left(S,V\right)\right)\\ \wedge \left(\forall i\in \mathrm{Fin}\left(k\right),\forall a\in C\left(\mathrm{apply}\left(o,i\right)\right),\left[\begin{array}{r}\left(R\left(V,a\right)=\mathrm{app}\left(\mathrm{take}\left(i,\mathrm{ofFn}\left(j\mapsto \mathrm{entry}\left(\mathrm{apply}\left(c,j\right),d\right)\right)\right),R\left(\mathrm{apply}\left(U,i\right),a\right)\right)\right)\\ \wedge \left(\mathrm{len}\left(R\left(V,a\right)\right)=i+\mathrm{len}\left(R\left(\mathrm{apply}\left(U,i\right),a\right)\right)\right)\end{array}\right]\right)\end{array}\right]\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Observer/Budget/ResidueChildPrefixStructure.residue_child_prefix_structure (✓ std3). ∎

Source. Repository-derived.

Commentary.

The first clause applies to every identifying original tree T. It produces a bijection o from Fin k to I, whole child trees U, prefixes P, centers c and continuations next. Every center c(i) belongs to its child and U(i) identifies that complete child. For every target a in it, the original trace is exactly P(i) followed by R(U(i),a). The prefix has at least i entries. When i+1<k, or when k=1 and d+1<e, U(i) has head c(i) and continuation next(i). There is no head requirement on the last child when k>1, nor on a singleton leaf. Whenever i<j, P(i) followed by entry(c(i),d) is a prefix of P(j). Consequently len(R(T,a))=len(P(i))+len(R(U(i),a)) is at least i+len(R(U(i),a)). Original constant delays are retained.

The second clause is independently universal in the bijection o and in the supplied child family U. Each U(i) identifies C(o(i)); only nonlast trees must have a head centered in their own child. The resulting c and next are those actual heads and continuations at nonlast positions. The parent V identifies S, and its trace at a target in child i is exactly the first i entries of List.ofFn(j maps to entry(c(j),d)), followed by the unchanged trace of U(i). Its length is i+len(R(U(i),a)). The final value c(k-1) is unused and unrestricted. In particular, no extra entry query is charged to the final child.

For extraction, structural induction on T simultaneously tracks the remaining child labels, their distinct exhaustive order, child identification and chronological prefixes. An outside center has a constant answer on the remaining state; this answer is prepended to all later prefixes. An inside center enters one child. Its entire query subtree is retained for that child, and its depth-d continuation handles the other labels. Keeping only one continuation inside the entered child would be incorrect: for p=2,e=2,d=0 and center zero, targets zero and two in the same child give answers two and one. A stop can identify the remaining state only when it is a singleton leaf. Thus a singleton nonleaf is normalized through its actual constant roots.

For realization, finite induction starts with the supplied last tree unchanged. At an earlier supplied head, only response d is redirected to the already constructed suffix. Within the head’s own child the answer differs from d, so the entire supplied trace is preserved. All other children answer d. These disjoint responses prove identification and give the exact prefix formula. For k=1 the construction is just U(0). Residue geometry is independent of a prior; a uniform positive rational prior suffices when applying its geometric conclusions. The result concerns actual protocol traces and makes no claim about selector termination, optimal horizons or assignment runtime.

References

• Truth anchor: D5/S3/Observer/Budget/ResidueChildPrefixStructure.residue_child_prefix_structure
• Dependency: D5/S3/Observer/Budget/ResiduePosteriorClosure