Internally maintained finite memory and the fixed-prior optimum
Abstract
A single-deflection finite-state controller attaining the actual marker-stopping minimum.
Theorem 1.1 (Complete finite and infinite threshold branches with actual-source refinement).
Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/SingleDeflectionOptimalController.single_deflection_optimal_controller (✓ std3). ∎
Source. Repository-derived.
Commentary.
The prior mu is any probability measure on the closed unit interval with 0<Q<1 almost everywhere, alpha is strictly between zero and one, and reciprocalMoment(mu) is finite. coefficient(alpha,mu,m) is the original integral of (1-Q)(alpha-(1-alpha)Q)Q^(m-1). N is the original WithTop infimum of positive negative-coefficient indices. Natural thresholds are embedded into WithTop in the formulas. The empty negative set has threshold infinity. Dirac priors, nondegenerate priors, zero coefficients and all ties remain within the same hypotheses.
The coefficient tail follows without a nondegeneracy assumption: alpha times v_m minus (1-alpha) times v_(m+1) is the integral of (1-Q)Q^(m-1)(alpha-(1-alpha)Q)^2, which is nonnegative. These polynomials are integrable on the compact unit interval. Thus a negative coefficient forces the next coefficient to be negative. The least positive negative index is Nat.find when such an index exists and equals the original WithTop infimum.
For finite N=k, C.Memory is Option Fin(2k-1+2), with 2k+2 total states including the marker sink. The initial state is some(machineEncode(2k-1,0)); a false reply applies the existing saturating machineUpdate, and a true reply enters none. The optional action is right exactly at the counter pulse and left in all other active states. For infinite N, C.Memory is Option Unit, initially some(unit), with the always-left action and the same absorbing marker sink. None emits no action. The delay is internal state, with no external clock input.
plannedSide(N,n) is right precisely when N=k is finite and n+1=2k; it is left otherwise. Thus the sole right query is the one-based query 2N. The actual controller updates its memory once per acquired reply. controlledRun records that memory and the environment’s acquired trace; the environment supplies the fresh-arm markerResponse using its queried arm counts. It does not supply a clock to the controller. In the formulas memory and trace are the first and second controlledRun projections.
controllerPolicy is the original measurable Policy adapter: it folds acquired replies chronologically from C.initial and reads C.action, using left as a dormant default when the action is none. The source histories are newest first, so the fold reverses the reply list. For every seed, source and horizon, controlledRun has exactly the original actualRun trace and its memory is exactly this reply fold. Its action is none exactly after stopping and otherwise is some(plannedSide(N,n)). The marker-producing query is included in the trace; the halted machine performs no later query.
At every positive even replay depth 2m, the same constructed policy has the joint left/right count pair (2m,0) before N and (2m-1,1) from N onward. Lambda is measured under the original arbitrary independent seed probability law, without survival conditioning, and equals the indicator of N<=m. The source execution refinement and the frozen exact counter readout are used to obtain these common-route counts.
expectedCost retains the original nonnegative integral of actual stoppingTime under priorLaw, the original prior bind of the independent-seed joint source law. The attained real cost is 2 reciprocalMoment(mu).toReal-(1-alpha) plus the absolutely summable sum of min(0,coefficient(alpha,mu,n+1)). Finiteness is established before converting to real costs. The extended expectation is no greater than that of every legal Policy on any other measurable seed space with any original independent probability law.
This is fixed-prior finite-state existence for choosing directions, immediate stopping and the mean objective. It gives no procedure to decide N from an arbitrary approximate prior representation, no finite exact predictor dimension, no optimal-policy uniqueness, no uniform state bound over priors and no state-minimality claim.