Prefix-Constrained Greedy Optimality

Abstract

Antitone gains on finite depth chains admit a prefix-closed maximizer under a unit-cost budget.

Theorem 1.1 (Top-gain cells can be repaired to a prefix optimum).

$$\begin{array}{c}\forall P:\mathrm{Type},\mathrm{Finite}(P),\\ d,B\in \mathbb{N},g:P\to \mathrm{Fin}(d)\to \mathbb{R},\\ Top:\mathrm{Finset}(P\times \mathrm{Fin}(d)),\\ (\forall p:P,\forall i,j\in \mathrm{Fin}(d),i\le j\Rightarrow g(p,j)\le g(p,i))\wedge \Vert Top\Vert =B\wedge \\ (\forall a\in Top,\forall b:P\times \mathrm{Fin}(d),\neg (b\in Top)\Rightarrow g(\mathrm{fst}(b),\mathrm{snd}(b))\le g(\mathrm{fst}(a),\mathrm{snd}(a)))\Rightarrow \\ \exists A:\mathrm{Finset}(P\times \mathrm{Fin}(d)),\\ \Vert A\Vert =B\wedge (\forall p:P,\forall j\in \mathrm{Fin}(d),(p,j)\in A\Rightarrow \forall i\in \mathrm{Fin}(d),i<j\Rightarrow (p,i)\in A)\wedge \\ \sum _{c\in Top}g(\mathrm{fst}(c),\mathrm{snd}(c))\le \sum _{c\in A}g(\mathrm{fst}(c),\mathrm{snd}(c))\wedge \\ (\forall C:\mathrm{Finset}(P\times \mathrm{Fin}(d)),\Vert C\Vert =B\Rightarrow \sum _{c\in C}g(\mathrm{fst}(c),\mathrm{snd}(c))\le \sum _{c\in A}g(\mathrm{fst}(c),\mathrm{snd}(c))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/ArithmeticTomography/PrefixConstrainedGreedyOptimality.prefix_constrained_greedy_optimality (✓ std3). ∎

Source. Repository-derived.

Commentary.

The channel type is finite and the available levels form Fin(d), so the candidate cell region is finite. Selecting B cells is exactly the budget constraint when every cell has unit cost.

Gain is publicly antitone along each channel. The selected set Top also satisfies the top-budget premise: every selected cell has gain at least that of every omitted cell.

Replacing a selected level whose predecessor is missing strictly lowers the sum of selected depth indices and cannot lower total gain. The process therefore terminates at a prefix-closed selection. Pairing the cells outside Top with the cells omitted from Top proves global optimality among all B-cell selections.

References

• Truth anchor: D5/S3/Observer/ArithmeticTomography/PrefixConstrainedGreedyOptimality.prefix_constrained_greedy_optimality