Semantic Sufficiency Beyond Finite Resources

Abstract

More semantic targets than allowed algorithms force a resource-unreachable target.

Theorem 1.1 (Semantic sufficiency can exceed finite resources).

$$\begin{array}{c}\forall X,B_C,Y:\mathrm{Type},[\mathrm{Fintype}\left(Y\right)],[\mathrm{Nonempty}\left(Y\right)],\\ C:X\to B_C,[\mathrm{Fintype}\left(\mathrm{range}\left(C\right)\right)],cost:ResourceCost,r\in \mathbb{N},\\ A_r:\mathrm{Finset}\left(B_C\to Y\right),\\ A_r=\{f:B_C\to Y\mid \mathrm{cost}\left(f\right)\le r\},\\ |Y{|}^{|\mathrm{range}\left(C\right)|}>|A_r|\Rightarrow \exists T:X\to Y,\\ \mathrm{Refines}\left(T,C\right)\wedge \neg \mathrm{ResourceRefines}\left(cost,r,T,C\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Refinement/SemanticResourceSeparation.semantic_sufficiency_can_exceed_finite_resources (✓ std3). ∎

Source. Repository-derived.

Commentary.

The target carrier and the image of the concept readout are finite, and the target carrier is nonempty. The finite allowed class is exactly the class of factor maps whose declared cost is within budget.

Restricting every allowed factor to the readout image yields no more functions than there are allowed algorithms. The strict cardinality hypothesis therefore supplies a target function missing from those restrictions.

Composing that function with the readout constructs the target. Nonemptiness extends the function off the image, proving semantic refinement, while membership in the budget class would contradict how it was selected.

References

• Truth anchor: D5/S3/ConceptDynamics/Refinement/SemanticResourceSeparation.semantic_sufficiency_can_exceed_finite_resources
• Dependency: D5/S3/ConceptDynamics/Refinement/ResourceRefinementComposition