Historical Processes and Depth-Budget Joint Extrema
Abstract
One iid law and one infinite greedy code attain the full-history depth-budget joint extremum.
Let A be the actual finite alphabet, with at least two letters and the full discrete measurable structure. The real parameter delta is positive and at most the reciprocal of the number of letters. Every row q(v,a), including the empty-history row, is normalized and bounded below by delta. Histories are complete finite words. No stationarity, finite memory, computability, rationality or summable-tail assumption is imposed. The function b gives arbitrary natural budgets at every depth.
NormalizedRows(q) means that all row entries are nonnegative and each row sums to one. For a proof h of this property, mu(q,h) denotes trajectoryLaw(q,h): its initial law is the row at the empty history; after coordinates zero through n, its successor kernel is the row at precisely that observed prefix of length n plus one. The cylinder C(w) fixes coordinates zero through length(w) minus one, so C of the empty word is the whole trajectory space. U(F) denotes deletedSet(F), the union of these cylinders. trunc(F,N) is the set of words in F of length at most N.
Legal(b,F) requires prefix freedom, excludes the empty word and bounds the number of distinct words of each length n by b(n). Fix any distinguished actual letter a with subscript zero. extremalVector(delta,a) assigns delta to every other letter and one minus the number of other letters times delta to that letter. In the formula, p is this vector and G is the one infinite greedyCode with mass priority and the prescribed tie order at each depth. truncatedMass is the finite word-mass sum through the given horizon, and codeMass is the total word-mass sum in the extended nonnegative reals. Lambda notation denotes a function, and const(B,z) is the standard constant function on B with value z.
historicalGap(delta,b) is one minus the supremum of the real deletion masses over all such rows and all legal codes. IsGreatest asserts both membership and an upper bound for every member of the displayed set. Both greatest-value clauses use actual measures; the real clause also supplies the probability-bounded conversion needed for the gap identity.
Theorem 1.1 (One law and one code attain all horizons and the joint supremum).
Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/HistoricalDepthBudgetJointExtremum.historical_depth_budget_joint_extremum (✓ std3). ∎
Source. Repository-derived.
Commentary.
For a fixed finite code, backward induction assigns payoff one to a selected node before testing the terminal depth, and zero to an unselected terminal node. A row with entries at least delta is bounded by putting its entire surplus on one child of maximal continuation value. These choices define one total heavy-child function on histories and lawful rows everywhere.
At each original node, swap its heavy child with the distinguished letter. Recursive transport is a bijection at every depth and preserves prefixes in both directions. Its inverse first recovers the original prefix and then uses that original node’s inverse swap. Consequently every depth budget is preserved and every live path product becomes exactly the iid product of its transported word. Finite iid optimality bounds the transported code.
The full-history trajectory calculation includes the empty cylinder and the initial letter without a dummy coordinate. Prefix-free cylinders are measurable and pairwise disjoint. Nonnegative finite sums and increasing unions connect finite comparison to the actual infinite deletion event. Finite optimizing rows and swaps may depend on the code and the horizon; no coherent limit of these choices is needed. Infinite attainment uses the fixed iid row and the same G for every horizon and for total mass.
Zero budgets, skipped depths, exhaustion, empty codes and horizon zero are included. At the uniform endpoint the surplus is zero, with no division by surplus and no unique-heavy-child requirement. Label-dependent code restrictions would require a separate invariance condition. This joint optimization does not assert greedy optimality for a fixed historical law.