Support, actual improving policies, and true expectation boundaries
Abstract
Beneficial marker deflection under an arbitrary shared-parameter prior.
Theorem 1.1 (Complete support criterion with all finite and infinite mean consequences).
Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/BeneficialMarkerDeflection.beneficial_marker_deflection (✓ std3). ∎
Source. Repository-derived.
Commentary.
Q is the coordinate on the closed unit interval; the prior is any probability measure with Q strictly between zero and one almost everywhere. Alpha is strictly interior. The essential supremum may equal one without being attained. Atomic and nonatomic priors are both included, and the support criterion assumes no finite reciprocal moment.
priorLaw is the prior bind of the existing jointLaw: one Q is shared by both outward Markov arms, the root is mixed once with true mass alpha, and the original measurable seed has its independent probability law. The proof establishes measurability of the existing trajectory law from finite prefix masses and measurable cylinders. A Policy chooses a fresh arm from its seed and acquired action and reply lists, and the existing actual execution stops at the first marker.
expectedCost is the nonnegative integral of the actual stoppingTime, embedded from WithTop natural numbers into extended nonnegative reals with infinity preserved. reciprocalMoment integrates the reciprocal of one minus Q. coefficient at m integrates (1-Q)(alpha-(1-alpha)Q)Q to power m-1. firstNegative is the infimum of positive indices with a negative coefficient, with infinity for the empty set. Lambda always uses the original seed law of the all-zero replay, without survival conditioning.
The improving witness ignores seed and replies and queries right only at acquired-history lengths 2N-1 and 2N, otherwise left. An induction at every replay depth proves its even odd-odd probability is one exactly at N. A marker before the second planned right query still stops the actual execution immediately. History length is acquired internal information; the policy has no hidden-Q input or external clock.
Finite costs use their toReal values in the correction formula and comparison. The comparison permits different arbitrary measurable seed spaces and probability laws. When the reciprocal moment is infinite, every actual expectation is infinite, so the absolutely summable signed coefficients do not represent a difference of infinite expectations or a strict improvement of that objective.