Maximum Factor-Compatible Subdomain

Abstract

Largest target-consistent fiber blocks give the sharp factor-compatible domain size.

Theorem 1.1 (Largest target blocks give the exact compatible-domain size).

$$\forall X\in Type,B\in Type,Y\in Type,C\in X\to B,T\in X\to Y,\mathrm{Fintype}\left(X\right)\Rightarrow \left(\left(\forall A\in \mathrm{Finset}\left(X\right),\left(\forall x\in X,y\in X,\left(\left(x\in A\wedge y\in A\right)\wedge C\left(x\right)=C\left(y\right)\right)\Rightarrow T\left(x\right)=T\left(y\right)\right)\Rightarrow \mathrm{card}\left(A\right)\le \mathrm{sum}\left(b,\mathrm{image}\left(C,X\right),\max \left(r,\left\{C\left(r\right)=b\mid r\in X\right\},\mathrm{card}\left(\left\{C\left(x\right)=b\wedge T\left(x\right)=T\left(r\right)\mid x\in X\right\}\right)\right)\right)\right)\wedge \left(\exists A\in \mathrm{Finset}\left(X\right),\left(\forall x\in X,y\in X,\left(\left(x\in A\wedge y\in A\right)\wedge C\left(x\right)=C\left(y\right)\right)\Rightarrow T\left(x\right)=T\left(y\right)\right)\wedge \mathrm{card}\left(A\right)=\mathrm{sum}\left(b,\mathrm{image}\left(C,X\right),\max \left(r,\left\{C\left(r\right)=b\mid r\in X\right\},\mathrm{card}\left(\left\{C\left(x\right)=b\wedge T\left(x\right)=T\left(r\right)\mid x\in X\right\}\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/TargetRisk/MaximumFactorCompatibleSubdomain.maximum_factor_compatible_subdomain (✓ std3). ∎

Source. Repository-derived.

Commentary.

The bound is constructed directly from the finite state carrier. For each realized concept value, it counts the largest joint concept-target block and then sums those maxima.

Fiberwise factorization makes every admitted concept fiber fit inside one such block. Conversely, selecting one maximizing target block in every realized concept fiber gives an admitted domain attaining the bound.

References

• Truth anchor: D5/S3/ConceptDynamics/TargetRisk/MaximumFactorCompatibleSubdomain.maximum_factor_compatible_subdomain
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition