Strict Kernel Novelty Criterion

Abstract

Strict kernel shrinkage is exactly semantic novelty of the added readout.

Theorem 1.1 (A readout is novel exactly when it splits an old kernel pair).

$$\begin{array}{c}\forall X,O:\mathrm{Type},\\ \Gamma :\mathrm{Set}(\mathrm{Concept}(X,O)),p:\mathrm{Concept}(X,O),\\ \mathrm{StrictSubset}(\mathrm{jointKernel}(\lambda d:\mathrm{insert}(p,\Gamma ),\mathrm{readout}(d)),\mathrm{jointKernel}(\lambda d:\Gamma ,\mathrm{readout}(d)))\iff \\ \neg (p\in \mathrm{SemanticClosure}(\Gamma )).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DefinitionEscapeLaws/StrictKernelNoveltyCriterion.strict_kernel_novelty_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Gamma is an output-valued concept family on X, and p is a candidate concept on the same carrier. SemanticClosure and jointKernel are the canonical imported objects.

The inserted-family kernel is always contained in the original kernel. The frozen zero-gain criterion identifies equality with closure membership, so inequality is exactly strict shrinkage.

References

• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeLaws/StrictKernelNoveltyCriterion.strict_kernel_novelty_criterion
• Dependency: D5/S3/ConceptDynamics/DefinitionEscapeLaws/SemanticClosureZeroGainCriterion