Compact Residual Finite Completion

Abstract

Compact open separation of a residual space is witnessed by a finite zero-spectrum budget.

Theorem 1.1 (Compact residual separation has a finite zero-spectrum settlement).

$$\begin{array}{r}\forall I,X,C,Y:\mathrm{Type},\\ V:I\to \mathrm{Type},\Gamma :\mathrm{Set}\left(I\right),\\ [\mathrm{TopologicalSpace}\left(X\times X\right)],\\ d:\forall i:I,\mathrm{Concept}\left(X,V\left(i\right)\right),\\ q:\mathrm{Concept}\left(X,C\right),T:\mathrm{Concept}\left(X,Y\right),\\ c:I\to \mathbb{R},\nu :\mathrm{EscapeWeight}\left(X\times X\right),\\ \mathrm{let}E=\mathrm{defectRelation}\left(q,T\right),K_a=\mathrm{conceptKernel}\left((d_i{)}_{i\in \Gamma },a\right),\\ U_a=\{e:E\mid \neg (e\in K_a)\},\\ \mathrm{IsCompact}\left(E\right)\wedge \\ \mathrm{intersection}\left(E,\mathrm{jointKernel}\left((d_i{)}_{i\in \Gamma }\right)\right)=\varnothing \wedge \\ (\forall a\in \Gamma ,\mathrm{IsOpen}\left(U_a\right))\wedge \\ (\forall i\in \Gamma ,0\le c\left(i\right))\Rightarrow \\ \exists S:\mathrm{Finset}\left(\Gamma \right),L:{\mathbb{R}}_{\ge 0},\\ L=\mathrm{finiteSelectionCost}\left(\Gamma ,c,S\right)\wedge \\ \mathrm{defectRelation}\left(\mathrm{conceptJoin}\left(q,\mathrm{finiteSelectionSupplement}\left(\Gamma ,d,S\right)\right),T\right)=\varnothing \wedge \\ \mathrm{finiteEscapeSpectrum}\left(\Gamma ,d,q,T,c,\nu ,L\right)=0.\end{array}$$

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

Source. Repository-derived.

Commentary.

The residual E is the canonical defectRelation of the baseline readout q against the target T. For each active definition, its cut U is represented as an open subset of the subtype E, so the openness premise is exactly relative openness.

Blind-kernel emptiness invokes the existing finite_cover_laws equivalence to obtain a cover of E. Compactness then extracts a Finset S of the active-definition subtype Gamma.

Nonnegative candidate costs make the exact sum C(S) an NNReal budget L. The selected supplement has empty target defect, so its residual mass is zero and the canonical finiteEscapeSpectrum at L is zero.

No continuity of the definitions, analytic compactness, positive baseline mass, optimizer, or infimum-attainment claim is used.

References

• Truth anchor: D5/S3/ConceptDynamics/EscapeSpectrum/CompactResidualFiniteCompletion.compact_residual_finite_completion
• Dependency: D5/S3/ConceptDynamics/EscapeSpectrum/BudgetEnvelopeCompletion