Blind Residual Charge Decomposition

Abstract

Every finite selected residual decomposes into its blind and finitely removable charge.

Theorem 1.1 (Finite residual charge splits around the common blind kernel).

$$\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,\mathrm{Concept}\left(X,V(i)\right),\\ q:\mathrm{Concept}\left(X,C\right),T:\mathrm{Concept}\left(X,Y\right),\\ c:I\to \mathbb{R},L:\mathrm{NNReal},\\ S:\mathrm{Finset}\left(\Gamma \right),A:\mathrm{Set}\left(\mathrm{Set}\left(X\times X\right)\right),\\ hA:\mathrm{IsSetRing}\left(A\right),\nu :\mathrm{AddContent}\left(\mathrm{NNReal},A\right),\\ \mathrm{Countable}\left(\Gamma \right)\wedge (\forall i\in \Gamma ,0<c(i))\wedge \\ 0\le \mathrm{coeReal}\left(L\right)\wedge 0<\nu (\mathrm{defectRelation}\left(q,T\right))\wedge \\ \mathrm{let}E=\mathrm{defectRelation}\left(q,T\right),B=\mathrm{intersection}\left(E,\mathrm{jointKernel}\left((d_i{)}_{i\in \Gamma }\right)\right),\\ U_a=\mathrm{intersection}\left(E,\mathrm{complement}\left(\mathrm{conceptKernel}\left((d_i{)}_{i\in \Gamma },a\right)\right)\right),E_S=\mathrm{defectRelation}\left(\mathrm{conceptJoin}\left(q,\mathrm{finiteSelectionSupplement}\left(\Gamma ,d,S\right)\right),T\right),\\ E\in A\wedge B\in A\wedge \\ (\forall a\in \Gamma ,U_a\in A)\Rightarrow \\ B=E\setminus \mathrm{iUnion}\left(a\in \Gamma ,U_a\right)\wedge \\ E_S=E\setminus \mathrm{iUnion}\left(a\in S,U_a\right)\wedge \\ B\subseteq E_S\wedge \\ E_S\in A\wedge \nu (B)\le \nu (E_S)\wedge \\ \nu (E_S)=\nu (B)+\nu (E_S\setminus B)\wedge \\ (\Gamma =\varnothing \Rightarrow E_S=E).\end{array}$$

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

Source. Repository-derived.

Commentary.

The baseline residual E is the canonical defectRelation. Each single-definition cut U and the blind residual B use the existing conceptKernel and dependent jointKernel; the finite residual E_S uses the canonical finiteSelectionSupplement.

The theorem first proves that B is exactly E outside the union of all language cuts. Agreement on every language coordinate then shows that B survives every finite selection S.

An AddContent with NNReal values on an arbitrary IsSetRing supplies finite additivity and monotonicity on the stated algebra. The residual, blind residual, and every single-definition cut are explicitly required to belong to that algebra.

The countable language, positive candidate costs, nonnegative budget, and positive baseline charge retain the source domain even though the local decomposition does not consume their numerical values. When Gamma is empty, the selected residual is the baseline residual; counting charge on a nonempty Boolean residual compiles all premises.

References

• Truth anchor: D5/S3/ConceptDynamics/EscapeSpectrum/BlindResidualChargeDecomposition.blind_residual_charge_decomposition
• Dependency: D5/S3/ConceptDynamics/EscapeSpectrum/BudgetEnvelopeCompletion