Passive Policy Normalization

Abstract

Deleting constant passive queries preserves terminal candidate fibers and outputs, does not increase any actual cost, and gives a minimax recursion by candidate cardinality.

Theorem 1.1 (Normalization and minimax with zero query costs).

$$\begin{array}{r}\mathrm{Finite}\left(Q\right)\wedge C\ne \varnothing \wedge \mathrm{freeC}\left(C\right)\wedge \mathrm{freeReply}\left(C\right)⟹\\ \forall \pi ,\mathrm{Feasible}\left(\pi ,C,B\right)⟹\exists p,d,\mathrm{Pruned}\left(C,p\right)\wedge \\ \forall x\in C,d(\tau (x))=l(x)\wedge \mathrm{out}\left(d(\tau (x))\right)=\mathrm{out}\left(l(x)\right)\wedge \mathrm{Sublist}\left(\tau (x),t(x)\right)\wedge \mathrm{length}\left(\tau (x)\right)\le \mathrm{card}\left(C\right)-1\wedge \\ C(\tau (x))=C(t(x))\wedge \mathrm{Legal}\left(C(\tau (x)),d(\tau (x))\right)\wedge K\left(\tau (x),d(\tau (x))\right)\le K\left(t(x),l(x)\right)\le B,\\ \forall x,z\in C,(\tau (x)=\tau (z)\iff t(x)=t(z));\\ V\left(B,C\right)=V\left(B,\mathrm{card}\left(C\right)-1,C\right),\\ A\left(B,C\right)=\{q\in Q\mid 2\le \mathrm{card}\left(\mathrm{answers}\left(C,q\right)\right)\wedge c\left(q\right)\le B\},\\ w\left(q\right)=\underset{y\in \mathrm{answers}\left(C,q\right)}{\max }e\left(V\left(B-c\left(q\right),\mathrm{fiber}\left(C,q,y\right)\right)\right),\\ e\left(V\left(B,C\right)\right)=\min \{e\left(r\left(B,C\right)\right),{\inf }_{q\in A\left(B,C\right)}w\left(q\right)\},\\ \forall q\in Q,2\le \mathrm{card}\left(\mathrm{answers}\left(C,q\right)\right)⟹\forall y\in \mathrm{answers}\left(C,q\right),\mathrm{card}\left(\mathrm{fiber}\left(C,q,y\right)\right)<\mathrm{card}\left(C\right),\\ A\left(B,C\right)=\varnothing ⟹{\inf }_{q\in A\left(B,C\right)}w\left(q\right)=\infty ,\\ A\left(B,C\right)\ne \varnothing ⟹\exists q\in A\left(B,C\right),{\inf }_{q\in A\left(B,C\right)}w\left(q\right)=w\left(q\right),\\ e\left(V\left(B,C\right)\right)=U\left(B,C\right)\ne \infty .\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Experiment/PassivePolicyNormalization.result (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let C be a finite nonempty set of complete sources in an arbitrary carrier W. Each run retains one source, including any shared noise, environment, or device state encoded in it. Let Q be a finite query family, possibly empty, with response type Y(q) depending on q and fixed readout read(q) from W to Y(q). Every query is available at every candidate set. Queries only read the source: they do not change it, unlock actions, or change the terminal contract.

A history is a finite list of query-response pairs. An arbitrary raw policy selects either a query or a terminal label from each history. Execution follows the response of the same source at every query. Only actual runs from C must terminate; no termination condition is imposed on impossible histories or sources outside C. Write t(x) and l(x) for the unique terminal history and label of an actual run.

Terminal labels lie in an arbitrary type L and are decoded by out into a metric space Z with finite distances; F maps sources to their target points in Z. Distinct labels may represent different implementations of the same output. Legal(D,l) and the terminal fee tp(D,l) depend on the candidate set D and label l. The query prices c(q) and terminal fees are natural numbers and may be zero. For a history h, C(h) consists of the sources in C matching every recorded response, and K(h,l) is the sum of its query prices plus tp(C(h),l). Feasible means that each actual run terminates with Legal(C(t(x)),l(x)) and K(t(x),l(x)) at most B.

Assume a legal label of terminal fee zero at C and at every nonempty one-query response fiber C(q,y). These are the hypotheses freeC and freeReply. A contract providing a free legal stop at every reachable history implies both. The latter contract also supplies the same hypotheses when the result is applied recursively to smaller candidate sets. No optimal terminal label is assumed to exist.

Every feasible raw policy has a dependent PassiveProtocol tree p and a history decoder d. Put tau(x) = runPassiveProtocol(read,p,x). The tree is pruned: each retained query has strictly smaller candidate sets in all response branches. On every actual run, tau(x) is a sublist of t(x), has length at most the cardinality of C minus one, and decodes to exactly l(x). Thus the output out(l(x)) is unchanged. Equality of compressed terminal histories is equivalent to equality of original terminal histories; the candidate fibers C(tau(x)) and C(t(x)) are equal. Terminal legality and the terminal fee are therefore preserved. The total cost on each source is no larger than its original cost and remains at most B.

The finite candidate set gives a common fuel bound for all terminating actual runs. Induction on this bound removes a query when its response is constant on the current candidates and otherwise joins the smaller response branches. The equality of terminal-history partitions lets the original labels factor through the compressed histories. Nonnegative query prices give the pathwise cost inequality. Each retained query strictly decreases the positive candidate cardinality, which gives the depth bound.

For any candidate set D, the risk of a feasible policy is the maximum over x in D of dist(out(l(x)),F(x)). Let V(B,D) be its real infimum over all pointwise terminating feasible policies and V(B,H,D) the infimum with at most H actual queries. Let r(B,D) be the real infimum of the same maximum error over legal labels whose terminal fee is at most B. Free stops make these feasible sets nonempty. Normalization gives V(B,C) = V(B,card(C)-1,C).

Let A(B,C) contain the queries with at least two realized responses and price at most B, and let C(q,y) be the corresponding nonempty response fiber. The continuation value w(q) is the maximum, over realized responses y, of V(B-c(q),C(q,y)), embedded into the extended nonnegative reals by e = ENNReal.ofReal. The minimax value is the minimum of e(r(B,C)) and the infimum of w(q) over A(B,C). An empty eligible query set contributes positive infinity; otherwise a query attains this finite-family infimum. This does not assert that any stopping radius or policy risk infimum is attained.

The value equality follows by splitting a pruned tree at its first query and joining choices on its finitely many realizable response fibers. Finite supremum-infimum exchange permits arbitrarily close choices without an optimal-center assumption. For every eligible query, each response fiber has smaller cardinality than C. Cardinality therefore makes the recursion well founded even when c(q) is zero. The extended value U(B,C), defined using the loss e(dist(out(l),F(x))), equals e(V(B,C)) and is not infinity. These statements concern fixed passive queries; they provide no complexity bound for finding a policy or a center and do not cover active actions whose availability or effects depend on history.

References

• Truth anchor: D5/S3/ConceptDynamics/Experiment/PassivePolicyNormalization.result
• Dependency: D5/S3/ConceptDynamics/Experiment/PassiveAdaptiveTranscriptUpperBound