Uniform discounted phase occupation
Abstract
Uniform discounted occupation of the actual phase-only renewal reader.
Theorem 1.1 (Exact uniform bounds for every moment, phase and finite cap).
Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/GeometricPhaseOccupation.uniform_discounted_phase_occupation
Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/GeometricPhaseOccupation.uniform_discounted_phase_occupation (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every natural m, every j at least one, and real s and eta satisfying s>0 and s times 2^j <= eta <= 1, let b_m=3 exp(-6)/2^(m+3) and B_m=exp(1)(m+1)!2^(m+1). Both constants are positive. The actual discounted occupation A_j is finite and satisfies b_m 2^(j(m+1)) <= A_j <= B_m 2^(j(m+1)). The quantifiers include m=0 and j=1.
The actual uncapped trajectory starts in phase one. Each actual zero makes one Bernoulli transition: source phase j advances with probability 2^(-j) and otherwise remains. Lean stores source phase j as natural index j-1. The observer state is only this phase. The trajectory measure is generated by the phase row using Mathlib trajMeasure; its marginals are identified with the iterated row laws using the existing MarkovPrefixMass supplier.
The entrance law of source phase one is pure zero. For analysis, entrance into the next phase is the sum of the previous entrance count and an independent geometric positive holding time. The pair law records the entrance count t and the current number w of failures before success. Its occupation interval is exactly max(1,t) <= k < t+w+1. The discounted weight at k=0 is defined to be zero, including when m=0. At every positive k the weight is k^m exp(-s k).
A proved renewal recurrence identifies the actual phase mass at every zero count with the geometric entrance-interval mass. Nonnegative summation then proves equality of actual trajectory occupation and the analytical expected finite interval sum. The bounds consume this equality. No holding variable or countdown is added to the observer, and the correspondence is a conclusion of the construction rather than a model assumption.
For the lower bound, Markov’s inequality gives probability at least 3/4 of entrance before 4 times 2^j. The independent holding time is at least 2^j with probability at least exp(-1), using the original geometric-tail declaration and the logarithmic lower bound. The 2^(j-1) integers from t+2^(j-1) to t+2^j-1 lie in the exact occupation interval, are at least one, and each contributes at least 2^((j-1)m) exp(-5). This yields exactly b_m.
For the upper bound, the binomial geometric series gives the positive holding moment bound E W^p <= p! (2^j)^p for every natural p. Binomial expansion and independence bound the entrance-sum moment by p! times the sum of holding means raised to p. Taking p=m+1 and bounding each finite occupation sum by its exit count to that power gives a bound at least as strong as the stated B_m.
For every natural finite cap J>=j, the actual capped row acts on Fin(J+1), with live source phases 1 through J and one absorbing dead state. Clamping the uncapped row commutes with this capped row and therefore with every iterated marginal law. Every capped live phase has exactly the uncapped discounted occupation. This includes J=j and J=j=1; there is no fixed cap or fixed moment restriction.