Definition Kernel Galois

Abstract

Family kernels form a Galois connection detecting primitive and productive escape.

Theorem 1.1 (Definition families and relations form a Galois connection).

$$\begin{array}{r}\forall X,Output:\mathrm{Type},\\ \forall Gamma:\mathrm{Set}\left(\mathrm{Concept}\left(X,Output\right)\right),\\ \forall relation:\mathrm{Set}\left(X\times X\right),\\ \mathrm{Subset}\left(Gamma,\mathrm{RelationInvariantReadouts}\left(relation\right)\right)⟺\mathrm{Subset}\left(relation,\mathrm{jointKernel}\left(\mathrm{definitionReadout}\left(Gamma\right)\right)\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DefinitionEscape/DefinitionKernelGalois.definition_relation_galois (✓ std3). ∎

Source. Repository-derived.

Commentary.

The theorem reuses the canonical RelationInvariantReadouts and jointKernel carriers. A family is invariant on a relation exactly when the relation is contained in the common kernel of every family member.

The two implications unpack the same pairwise equality in opposite directions. No auxiliary kernel or replacement readout is introduced.

Theorem 1.2 (Escaping the semantic closure is exactly having a kernel witness).

$$\forall X,InputOutput,Output:Type,Gamma:\mathrm{Set}\left(\mathrm{Concept}\left(X,InputOutput\right)\right),target:\mathrm{Concept}\left(X,Output\right),\neg (target\in \mathrm{SemanticClosure}\left(Gamma\right))⟺\exists left,right:X,(\forall definition:Gamma,\mathrm{definition}\left(left\right)=\mathrm{definition}\left(right\right))\wedge \mathrm{target}\left(left\right)\ne \mathrm{target}\left(right\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DefinitionEscape/DefinitionKernelGalois.not_mem_semanticClosure_iff_kernel_witness (✓ std3). ∎

Source. Repository-derived.

Commentary.

A readout lies outside the semantic closure of a family exactly when some pair of points is identified by every member of the family yet separated by the readout.

Both directions reuse the fiber-constancy characterisation of the closure. No new kernel, separator, or replacement readout is introduced.

References

• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscape/DefinitionKernelGalois.definition_relation_galois
• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscape/DefinitionKernelGalois.not_mem_semanticClosure_iff_kernel_witness
• Dependency: D5/S3/ConceptDynamics/DefinitionEscape/BlindKernelObstruction
• Dependency: D5/S3/ConceptDynamics/DefinitionEscape/ResidualJoinLaw