Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Exact Residue Fibers and Adaptive Posteriors

Abstract

Actual longest-congruence queries preserve singleton or sibling states, and conditioning a strictly positive rational prior on the executed history gives exactly those candidates.

Fix any prime p and any natural exponent e, including zero. Write X for ZMod(p^e), and let mu assign a strictly positive rational mass to every element of X, with total mass one. Write m(U) for the sum of mu over U and emb for the nonnegative extended-real embedding of a nonnegative rational number. The query h(c,a) is the existing residueReadout: the maximum of all k from zero through e for which the natural representatives agree modulo p^k. For each fixed p,e, put Z(k)=ZMod(p^k) for k in N and X=Z(e). The map pi(k,a), for k<=e and a in X, is primePowerProjection from precision e to k.

For d<=e and b in Z(d), B(d,b) is the complete fiber pi(d,a)=b. For d<e and b in Z(d), Ch(d,b) consists of all labels modulo p^(d+1) reducing to b. For any I in Fin(Z(d+1)), S(d,I) is the union of their complete fibers in X. Empty I is permitted in a fiber formula; a sibling state requires I nonempty. For every S in Fin(X), c in X, and r in N, define F(S,c,r) as the elements a of S with h(c,a)=r, and R(c,r)=F(X,c,r). For t<e and c in X, J(t,c) is Ch(t,pi(t,c)) with pi(t+1,c) removed. Shape(U) means that U is a singleton or S(d,I) for some d<e, parent b, and nonempty I contained in Ch(d,b).

A selector D takes the entire chronological list of pairs (center,response) and returns either the next center or none to stop. For each such D, natural n, and starting history P, U(D,n,P) is its finite unrolling into PassiveProtocol, beginning with accumulated history P and allowing n further queries. A query appends its actual reply before the next selection. Trace denotes runPassiveProtocol with h. Run is Trace followed by the pointwise conversion from Sigma responses to pairs. Legal(D,P,H) means each center in H is selected by D on P followed by exactly the earlier pairs of H. C(H) is the intersection of the recorded reply equations. A(D,H) is defined separately as the targets whose actual run U(D,|H|,[]) equals H. It does not use C(H). Write L=List(X times N) and Sel for the maps from L to Option(X); nil is the empty history and snoc(H,c,r) appends the pair (c,r). Every history variable below ranges over L.

In the formula, apply(f,a) means f(a), and Fin(Y) denotes the finite subsets of Y, Union(I,f) the union of f(j) over j in I, and range(e+1) the natural numbers zero through e. For every finite T contained in X, m(T) is the sum of mu(a) over a in T; for every PMF P on X, prob(P,T) is the sum of P(a) over a in T. Supported(P,T) means there exists a in T belonging to support(P). The expression filter(P,T,hs) denotes PMF.filter using a witness hs of Supported(P,T). The witnesses hn, hs, hF, hR in the formula respectively certify normalization and the indicated support intersections. A let binding extends only over its bracketed body; each bracketed list is an explicit conjunction. All notation in the formula is relative to its quantified p,e,mu; no history or response is fixed implicitly.

Theorem 1.1 (Complete fibers, execution events, and conditioning).

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

Source. Repository-derived.

Commentary.

The displayed assertions hold for all objects in the indicated ranges. Every complete node at depth d has p^(e-d) leaves. Every nonleaf parent has exactly p children, these complete child fibers are pairwise disjoint, and their union is the parent. S(d,I) is their union for every I. The root at depth zero is all X for every root label, so a center outside that parent is impossible.

For every d<e, parent b, I contained in Ch(d,b), and center c, S(d,I) is contained in B(d,b). If c is in B(d,b) but outside S(d,I), all current targets answer d. If c is outside B(d,b), choose any b0 in that complete parent: h(c,b0)<d and h(c,a)=h(c,b0) for every a in B(d,b). For nonempty I and c outside S(d,I), precisely one response fiber is S(d,I) and every other response fiber is empty.

If c belongs to S(d,I), its child label is pi(d+1,c). The depth-d fiber is S(d,I with that label removed), including when it is empty; it is nonempty exactly when another active child remains. For every d<t<e the response-t fiber is S(t,J(t,c)), with exactly p-1 complete nonpath children and positive cardinality. The response-e fiber is the singleton c; responses below d or above e have empty fibers. For every finite S, all distinct response fibers are disjoint and the fibers indexed from zero through e exhaust S.

Each active child of a depth-d parent has the same remaining height e-(d+1) and exactly p^(e-(d+1)) leaves. If d+1=e, every active child has one leaf. Otherwise d+1<e and every active child has more than one leaf. This quantifies over every active child, including a layer with only one active child. Such a child can still be nonleaf. Different response fibers may belong to different depths.

The execution equivalence holds for every starting history P, every continuation H, and every target. The prefix identity holds for every n<=m and also before conversion of Sigma responses to pairs. For every legal H, A(D,H)=C(H). If D selects c after H, then A(D,H followed by (c,r)) equals F(C(H),c,r). No equation identifies an intermediate prefix with a completed longer transcript.

Every nonempty candidate set C(H), even before choosing a selector, has Shape. At e=0, X is the singleton zero and mu assigns it mass one. At positive e, X is the union of all p first children. A nonempty response fiber of a singleton equals that singleton. Induction on chronological extensions uses the exact fibers and does not require strict shrinkage. Thus repetitions, constant queries, arbitrary history adaptation, stopping, and singleton continuations are all allowed; every finite prefix of a terminating strategy is included.

The prior is PMF.ofFintype applied to emb(mu(a)), with its normalization proved from the rational total. Its support is all X. For any D,H with m(A(D,H))>0, the theorem first derives Legal(D,[],H), then A(D,H)=C(H), nonemptiness, and Shape(C(H)). The posterior P is PMF.filter of that prior on the actual event A(D,H). Its support equals C(H). At each candidate a its value is emb(mu(a)/m(C(H))), and outside C(H) its value is zero.

Every nonempty finite leaf set has positive original mass. In a positive current history, let F=F(C(H),c,r) be nonempty. The response probability, the sum of P on R(c,r), is emb(m(F)/m(C(H))) and is strictly positive. Filtering P on the raw response event R(c,r) equals filtering the original prior on F. Its values are emb(mu(a)/m(F)) on F and zero elsewhere. When D actually selects c, the operational extension equality identifies F with the next actual event as well. This is sequential conditioning of the original prior.

For positive e, the bound, threshold, and top-depth equality follow from PrimePowerNonadaptiveResolution by identifying cast equality with equality of representative remainders. At e=0 these facts reduce to ZMod(1). Surjectivity of the natural projections and equal additive-homomorphism fiber sizes give the exact counts. The explicit fiber classification then drives the chronological induction. Strict positivity ensures conditioning removes no candidate except through a failed reply equation. Zero-mass priors are outside the assumptions: on two leaves, masses one and zero already give a probability support strictly smaller than the initial logical candidate set.

References