Budget Envelope Completion

Abstract

Nonnegative budget layers are cofinal among finite residual families, so their escape envelope converges to the all-finite infimum.

Theorem 1.1 (The finite-family budget envelope has the all-finite limit).

$$\begin{array}{r}\forall I,X,C,Y:\mathrm{Type},\\ V:I\to \mathrm{Type},Gamma:\mathrm{Set}\left(I\right),\\ d:\forall i:I,X\to V\left(i\right),\\ q:X\to C,T:X\to Y,\\ c:I\to \mathbb{R},nu:\mathrm{EscapeWeight}\left(X\times X\right),\\ \mathrm{let}{M}_0=\mathrm{mass}\left(nu,\mathrm{defectRelation}\left(q,T\right)\right),m\left(S\right)=\mathrm{mass}\left(nu,\mathrm{defectRelation}\left(\mathrm{conceptJoin}\left(q,\mathrm{finiteSelectionSupplement}\left(Gamma,d,S\right)\right),T\right)\right),\\ C\left(S\right)=\mathrm{finiteSelectionCost}\left(Gamma,c,S\right),\\ M\left(L\right)=\mathrm{sInf}\left(\{m\left(S\right)\mid S\in \mathrm{Finset}\left(Gamma\right),C\left(S\right)\le L\}\right),\\ \mathrm{rho}\left(L\right)=\frac{M\left(L\right)}{M_0},m_{\ast }=\mathrm{sInf}\left(\{m\left(S\right)\mid S\in \mathrm{Finset}\left(Gamma\right)\}\right),\\ 0<M_0\wedge \mathrm{Monotone}\left(\mathrm{mass}\left(nu\right)\right)\Rightarrow \\ \mathrm{Antitone}\left(M\right)\wedge \\ (\forall L:{\mathbb{R}}_{\ge 0},0\le M\left(L\right)\le M_0)\wedge \\ \mathrm{sInf}\left(\{M\left(L\right)\mid L\in {\mathbb{R}}_{\ge 0}\}\right)=m_{\ast }\wedge \\ \mathrm{Tendsto}\left(M,atTop,\mathrm{nhds}\left(m_{\ast }\right)\right)\wedge \\ \mathrm{sInf}\left(\{\mathrm{rho}\left(L\right)\mid L\in {\mathbb{R}}_{\ge 0}\}\right)=\frac{m_{\ast }}{M_0}\wedge \\ \mathrm{Tendsto}\left(rho,atTop,\mathrm{nhds}\left(\frac{m_{\ast }}{M_0}\right)\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/EscapeSpectrum/BudgetEnvelopeCompletion.budget_envelope_infimum_and_limit (✓ std3). ∎

Source. Repository-derived.

Commentary.

A candidate is a Finset of the active definition subtype Gamma. Its cost uses the canonical finiteSelectionCost, and its residual mass uses the canonical finiteSelectionSupplement, concept join, and target-defect relation.

Every finite candidate is feasible at some nonnegative-real budget, while every budget layer contains only finite candidates. These two directions identify the infimum across budget layers with the infimum across all finite candidates.

Antitonicity and the common greatest lower bound give the filter-level limit atTop. Dividing by the positive baseline mass preserves the infimum and limit for the normalized escape spectrum.

The theorem asserts approximation by cofinal budget layers only. It does not assert that any finite candidate attains either infimum.

References

• Truth anchor: D5/S3/ConceptDynamics/EscapeSpectrum/BudgetEnvelopeCompletion.budget_envelope_infimum_and_limit
• Dependency: D5/S3/ConceptDynamics/DefinitionEscape/FiniteCoverCounting