Semantic Closure Topology Invariance

Abstract

Semantic closure adds recoverable readouts without changing family observation topology.

Theorem 1.1 (Definition closure leaves family partition topology unchanged).

$$\forall Gamma:\mathrm{Set}\left(\mathrm{Concept}\left(X,Output\right)\right),\mathrm{partitionTopology}\left(\mathrm{familyReadout}\left(\mathrm{DefinitionClosure}\left(Gamma\right)\right)\right)=\mathrm{partitionTopology}\left(\mathrm{familyReadout}\left(Gamma\right)\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ObservationTopology/SemanticClosureTopologyInvariance.partitionTopology_definitionClosure_eq (✓ std3). ∎

Source. Repository-derived.

Commentary.

The family readout evaluates every definition in the supplied family at once. Its kernel records pairs on which all family members agree.

DefinitionClosure adds exactly the readouts recoverable from the old family. The imported kernel theorem shows that these additions do not change the joint kernel.

Readouts with the same kernel induce the same partition topology. Hence the closed family and original family have equal observation topologies, not merely comparable ones.

References

• Truth anchor: D5/S3/ConceptDynamics/ObservationTopology/SemanticClosureTopologyInvariance.partitionTopology_definitionClosure_eq
• Dependency: D5/S3/ConceptDynamics/DefinitionEscape/DefinitionKernelGalois
• Dependency: D5/S3/ConceptDynamics/ObservationTopology/PartitionTopologyKernel