Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Terminal Histories and Exact First-Step Costs

Abstract

Original rational cost attains its minimum over all eventually terminating deterministic history selectors, with exact sibling first-step recurrences.

Fix a prime p, a natural exponent e, and X=ZMod(p^e). The prior mu:X->Q is strictly positive at every state and has total mass one. Put q(c,a)=residueReadout(p,e,c,a) and m(S)=sum of mu(a) over a in S. Every cost below uses this original mu. Fin(X) denotes finite subsets of X; X itself also denotes the full finite set when used as an argument of m or K. For d<=e, B(d,j) is the full projection fiber with label j in Z(d)=ZMod(p^d). Ch(d,b) is the set of next-depth labels over b, and S(d,I) is the union of B(d+1,j) for j in I. Write C(d,j)=B(d+1,j) and E(d,I,j)=S(d,I with j removed).

Let L=List(X times N), Sel=L->Option(X), and Tree=PassiveProtocol(X,constant N). A tree is inductively well-founded; its infinitely many possible natural-answer branches need not have a common depth bound. Run(T,a) is the entire list of center-answer pairs obtained from runPassiveProtocol(q,T,a). Trace(T,a) is the same run before conversion from Sigma responses to pairs. Length is preserved by that conversion. U(D,n,P) is the existing unroll, permitting n further queries after the chronological prefix P. Term(D,P,a,H) means legal(D,P,H), q(c,a)=r for every (c,r) in H, and D(P++H)=none. It requires actual stopping, not just exhaustion of n. Lengths count only H, never the prefix P.

D_T is treeSelector(T): a stopped tree returns none on every history; a query node with center c returns some c on the empty history, and on (c’,r)::H follows its r branch if c’=c, otherwise returning none. Extra records after a stopped node also return none. A matching but impossible answer follows the given branch. General source selectors D remain arbitrary: repeated, outside, useless, and post-identification queries are allowed, and termination is required only on the finite set under consideration.

PC(S,P) is the set of rational values sum over a in S of mu(a)*length(H(a)), where D ranges over Sel and H ranges over functions X->L, every H(a) for a in S satisfies Term(D,P,a,H(a)), and zero error means that for every a,b in S and every common L0, Term(D,P,a,L0) and Term(D,P,b,L0) imply a=b. There is no condition on H outside S. TC(S) is the set of sums of mu(a)*length(Trace(T,a)) over S for all trees T whose traces distinguish every pair of states in S. These two sets are defined independently. Unique terminal histories make their lengths exactly the actual stopping counts.

In the formula, Values(I,j->f(j)) denotes the set of f(j) for j in I, and Divide(A,m) denotes the set of w/m for w in A. Least(A,k) means IsLeast(A,k), including membership, so every minimum displayed is attained. The bracketed lists are conjunctions. All notation is relative to the quantified p,e,mu; every D,P,a,H,n and every state set is quantified explicitly.

Theorem 1.1 (Exact selector costs, attained minima, and sibling recurrences).

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

Source. Repository-derived.

Commentary.

Terminal persistence is an induction on the legal suffix, allowing an arbitrary prefix and any larger horizon. The converse follows the residual selector through chronological prefixes by tree recursion. Two terminal histories for the same target agree at a common larger horizon. Taking the maximum of the realized lengths on a finite set gives simultaneous equality of complete traces and counts for every sufficiently large horizon. This maximum never ranges over all syntactic answer branches.

A separating query tree exists because center a separates a from every different state: its top-depth answer characterizes equality. At e=0, the carrier is a singleton and the stopped tree suffices. For each finite S, multiply all costs by the positive product of the rational denominators on S. The resulting objective is a natural-number weighted sum of actual query counts and therefore has an attained minimum. Positive scaling preserves the original rational ordering. The exact trace correspondence then gives attainment for all source selectors, at every prefix P.

An optimum on a sibling state with more than one leaf cannot stop or begin outside that state. An outside center has a constant answer, and deleting it preserves identification while subtracting the strictly positive mass of the state. For a center in child C, the parent-depth answer leaves exactly the complementary sibling set E. Restricting the optimum to C already includes the first query; restricting its miss branch to E leaves one additional query for each target in E.

For a nonleaf C, take its attained internal tree query(c,next) with c in C and an attained tree R for E. The splice query(c,r->if r=d then R else next(r)) has exactly the internal tree’s complete trace on C. On E its trace is (c,d) followed by R’s trace. It identifies the union, with cost K(C)+K(E)+m(E). Thus only the complement pays the extra entry query. When I has one nonleaf child, the state is that child itself and there is no extra entry charge. For leaf children and at least two active labels, every target pays the first query, giving m(S)+K(E); a singleton leaf requires zero queries.

The normalized full-root minimum E_mu(p,e) is K(X), since PC(X,[]) is precisely its source cost set and m(X)=1. For every nonempty S, dividing by its positive original mass gives the attained conditional minimum K(S)/m(S). Empty S has cost zero, and e=0 also has root cost zero. The result makes no claim about finite-horizon assignments, pointwise scheduling order, or algorithmic complexity.

References