Weighted Identification of Sibling Residue Leaves

Abstract

The least positive-weighted cost of identifying sibling residue leaves is attained by scanning in decreasing mass order and inferring the last leaf.

Fix a prime p and a natural number d. Let X be ZMod of p to the power d plus one. The actual response h(c,a) is the maximum index i from zero through d plus one for which the canonical natural representatives of a and c agree modulo p to the power i. The response q(c,a) is the Boolean equality test. Candidates S share one residue modulo p to the power d, and m assigns a strictly positive rational mass to each candidate. No normalization of these masses is required.

P is PassiveProtocol X with natural-number responses. R(T,a) means runPassiveProtocol h T a. I(T,S) means that equal R transcripts for two members of S imply equal targets. C(T,a) is the list of centers in R(T,a), and L(T,a) is its length. For an enumeration u from Fin k onto S, E(u,a) is the center list of the equality scan of List.ofFn of u, executed at a. Elements of S in these formulas are coerced to X. Set V contains exactly the rational costs of actual identifying protocols, as defined below.

Theorem 1.1 (Schedule attainment and the actual weighted minimum).

$$\begin{array}{r}\forall p,d:\mathbb{N},\mathrm{Prime}\left(p\right)\Rightarrow \\ X=\mathrm{ZMod}\left(p^{d+1}\right),\forall S:\mathrm{Finset}\left(X\right),\\ (\forall a\in S,\forall b\in S,\mathrm{ModEq}\left(p^d,\mathrm{val}\left(a\right),\mathrm{val}\left(b\right)\right))\Rightarrow \\ \forall m:X\to \mathbb{Q},(\forall a\in S,0<m\left(a\right))\Rightarrow \\ k=\mathrm{card}\left(S\right),\forall o:\mathrm{Equiv}\left(\mathrm{Fin}\left(k\right),S\right),\mathrm{Antitone}\left((i\mapsto m\left(o\left(i\right)\right))\right)\Rightarrow \\ V=\{\sum _{a:S}m\left(a\right)L\left(T,a\right)\mid T:P,I\left(T,S\right)\},\\ (\forall u:\mathrm{Equiv}\left(\mathrm{Fin}\left(k\right),S\right),\exists T:P,I\left(T,S\right)\wedge \\ (\forall i:\mathrm{Fin}\left(k\right),L\left(T,u\left(i\right)\right)=\min \left(\mathrm{val}\left(i\right)+1,k-1\right))\wedge \\ (\forall a\in S,C\left(T,a\right)=E\left(u,a\right)))\wedge \\ \mathrm{IsLeast}\left(V,\sum _{i:\mathrm{Fin}\left(k\right)}m\left(o\left(i\right)\right)\min \left(\mathrm{val}\left(i\right)+1,k-1\right)\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

A full-depth answer detects the queried leaf. All other sibling candidates give the same answer at a fixed center, including a center outside the candidate set. Relabeling continuation branches therefore converts actual and equality protocols in both directions while preserving every queried center and each target’s count. Identification is retained.

The equality scan attains the capped position count. Conversely, the equality-query normal form supplies a schedule no slower at any target than a given identifying tree. Multiplying by positive masses preserves that lower bound, and the rearrangement inequality minimizes the schedule cost by pairing decreasing masses with increasing coefficients. This proves both membership in V and its lower-bound property.

For one candidate the coefficient is zero. For k at least two the coefficients are one through k minus two, followed by k minus one twice. Thus the last pair may exchange places without changing cost; earlier unequal coefficients favor the larger mass. A sorted enumeration begins with a maximum mass candidate. With two leaves every enumeration costs one query at either target. The last survivor is inferred without an extra query.

References

• Truth anchor: D5/S3/Observer/Budget/ResidueLeafOptimality.leaf_sibling_weighted_minimum
• Dependency: D5/S3/Observer/Budget/EqualityQueryScheduleNormalForm