Resolvent Frontier Geometry

Abstract

Convex mixing of positive spectral completions controls both the white-floor frontier and its minimal resolvent cost.

Theorem 1.1 (Basic properties of the budget frontier).

$$\forall a\in \mathrm{Real}\left(\right),localMatches\in \mathrm{Real}\left(\right)\to \left(\mathrm{Measure}\left(\mathrm{Real}\left(\right)\right)\to Prop\right),resolventBudget\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right)\to \mathrm{Real}\left(\right),whiteFloor\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right)\to \mathrm{Real}\left(\right),fullFloor\in \mathrm{Real}\left(\right)\to \mathrm{Real}\left(\right),mix\in \mathrm{Real}\left(\right)\to \left(\mathrm{Real}\left(\right)\to \left(\mathrm{Measure}\left(\mathrm{Real}\left(\right)\right)\to \left(\mathrm{Measure}\left(\mathrm{Real}\left(\right)\right)\to \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right)\right)\right)\right),\left(a>0\wedge \left(\left(\forall nu\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),0\le \mathrm{apply}\left(resolventBudget,nu\right)\right)\wedge \left(\left(\forall nu\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),0\le \mathrm{apply}\left(whiteFloor,nu\right)\right)\wedge \left(\left(\forall L\in \mathrm{Real}\left(\right),nu\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),\mathrm{applyTwo}\left(localMatches,L,nu\right)\Rightarrow \mathrm{apply}\left(whiteFloor,nu\right)\le \mathrm{apply}\left(fullFloor,L\right)\right)\wedge \left(\left(\forall nu\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),\mathrm{div}\left(\mathrm{apply}\left(whiteFloor,nu\right),\mathrm{mul}\left(2,a\right)\right)\le \mathrm{apply}\left(resolventBudget,nu\right)\right)\wedge \left(\left(\forall L1\in \mathrm{Real}\left(\right),L2\in \mathrm{Real}\left(\right),nu\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),L1\le L2\Rightarrow \left(\mathrm{applyTwo}\left(localMatches,L2,nu\right)\Rightarrow \mathrm{applyTwo}\left(localMatches,L1,nu\right)\right)\right)\wedge \left(\left(\forall p\in \mathrm{Real}\left(\right),q\in \mathrm{Real}\left(\right),L\in \mathrm{Real}\left(\right),nu1\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),nu2\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),\left(0\le p\wedge \left(0\le q\wedge \left(\mathrm{add}\left(p,q\right)=1\wedge \left(\mathrm{applyTwo}\left(localMatches,L,nu1\right)\wedge \mathrm{applyTwo}\left(localMatches,L,nu2\right)\right)\right)\right)\right)\Rightarrow \mathrm{applyTwo}\left(localMatches,L,\mathrm{applyFour}\left(mix,p,q,nu1,nu2\right)\right)\right)\wedge \left(\left(\forall p\in \mathrm{Real}\left(\right),q\in \mathrm{Real}\left(\right),nu1\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),nu2\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),\mathrm{apply}\left(resolventBudget,\mathrm{applyFour}\left(mix,p,q,nu1,nu2\right)\right)=\mathrm{add}\left(\mathrm{mul}\left(p,\mathrm{apply}\left(resolventBudget,nu1\right)\right),\mathrm{mul}\left(q,\mathrm{apply}\left(resolventBudget,nu2\right)\right)\right)\right)\wedge \left(\forall p\in \mathrm{Real}\left(\right),q\in \mathrm{Real}\left(\right),nu1\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),nu2\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),\left(0\le p\wedge \left(0\le q\wedge \mathrm{add}\left(p,q\right)=1\right)\right)\Rightarrow \mathrm{add}\left(\mathrm{mul}\left(p,\mathrm{apply}\left(whiteFloor,nu1\right)\right),\mathrm{mul}\left(q,\mathrm{apply}\left(whiteFloor,nu2\right)\right)\right)\le \mathrm{apply}\left(whiteFloor,\mathrm{applyFour}\left(mix,p,q,nu1,nu2\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow \mathrm{let}frontierValues=L:\mathrm{Real}\left(\right)\mapsto C:\mathrm{Real}\left(\right)\mapsto \left\{\exists nu\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),\mathrm{applyTwo}\left(localMatches,L,nu\right)\wedge \left(\mathrm{apply}\left(resolventBudget,nu\right)\le C\wedge r=\mathrm{apply}\left(whiteFloor,nu\right)\right)\mid r\in \mathrm{Real}\left(\right)\right\},\mathrm{let}costValues=L:\mathrm{Real}\left(\right)\mapsto lambda:\mathrm{Real}\left(\right)\mapsto \left\{\exists nu\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),\mathrm{applyTwo}\left(localMatches,L,nu\right)\wedge \left(lambda\le \mathrm{apply}\left(whiteFloor,nu\right)\wedge c=\mathrm{apply}\left(resolventBudget,nu\right)\right)\mid c\in \mathrm{Real}\left(\right)\right\},\mathrm{let}feasibleBudgets=L:\mathrm{Real}\left(\right)\mapsto \left\{\mathrm{Nonempty}\left(\mathrm{applyTwo}\left(frontierValues,L,C\right)\right)\mid C\in \mathrm{Real}\left(\right)\right\},\mathrm{let}feasibleFloors=L:\mathrm{Real}\left(\right)\mapsto \left\{\mathrm{Nonempty}\left(\mathrm{applyTwo}\left(costValues,L,lambda\right)\right)\mid lambda\in \mathrm{Real}\left(\right)\right\},\mathrm{let}frontier=L:\mathrm{Real}\left(\right)\mapsto C:\mathrm{Real}\left(\right)\mapsto \mathrm{sSup}\left(\mathrm{applyTwo}\left(frontierValues,L,C\right)\right),\mathrm{let}minimalCost=L:\mathrm{Real}\left(\right)\mapsto lambda:\mathrm{Real}\left(\right)\mapsto \mathrm{sInf}\left(\mathrm{applyTwo}\left(costValues,L,lambda\right)\right),\left(\forall L\in \mathrm{Real}\left(\right),C\in \mathrm{Real}\left(\right),C\in \mathrm{apply}\left(feasibleBudgets,L\right)\Rightarrow \left(0\le \mathrm{applyTwo}\left(frontier,L,C\right)\wedge \mathrm{applyTwo}\left(frontier,L,C\right)\le \min \left(\mathrm{apply}\left(fullFloor,L\right),\mathrm{mul}\left(\mathrm{mul}\left(2,a\right),C\right)\right)\right)\right)\wedge \left(\left(\forall L\in \mathrm{Real}\left(\right),\mathrm{MonotoneOn}\left(\mathrm{apply}\left(frontier,L\right),\mathrm{apply}\left(feasibleBudgets,L\right)\right)\right)\wedge \left(\left(\forall L\in \mathrm{Real}\left(\right),\mathrm{ConcaveOn}\left(\mathrm{Real}\left(\right),\mathrm{apply}\left(feasibleBudgets,L\right),\mathrm{apply}\left(frontier,L\right)\right)\right)\wedge \left(\left(\forall C\in \mathrm{Real}\left(\right),\mathrm{AntitoneOn}\left((L:\mathrm{Real}\left(\right)\mapsto \mathrm{applyTwo}\left(frontier,L,C\right)),\left\{\mathrm{Nonempty}\left(\mathrm{applyTwo}\left(frontierValues,L,C\right)\right)\mid L\in \mathrm{Real}\left(\right)\right\}\right)\right)\wedge \left(\left(\forall L\in \mathrm{Real}\left(\right),\mathrm{MonotoneOn}\left(\mathrm{apply}\left(minimalCost,L\right),\mathrm{apply}\left(feasibleFloors,L\right)\right)\right)\wedge \left(\forall L\in \mathrm{Real}\left(\right),\mathrm{ConvexOn}\left(\mathrm{Real}\left(\right),\mathrm{apply}\left(feasibleFloors,L\right),\mathrm{apply}\left(minimalCost,L\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/Budget/ResolventFrontierGeometry.resolvent_frontier_basic_properties (✓ std3). ∎

Source. Repository-derived.

Commentary.

Nested conditional-supremum bounds prove concavity without an optimizer. The dual conditional-infimum argument proves convexity of minimal cost, while local-reading nesting gives window antitonicity.

References

• Truth anchor: D5/S3/Weil/Budget/ResolventFrontierGeometry.resolvent_frontier_basic_properties
• Dependency: D5/S3/Weil/ZetaAnalytic/FiniteWindowGlobalBoundary