Observation Escape Topology

Abstract

Kernel refinement and productive separation include empty-source primitive escape.

Theorem 1.1 (Primitive escape is strict partition refinement).

$$\begin{array}{c}\forall X,InputOutput,Output:\mathrm{Type},\\ Gamma:\mathrm{Set}\left(\mathrm{Concept}\left(X,InputOutput\right)\right),\\ candidate:\mathrm{Concept}\left(X,Output\right),\\ (\mathrm{PrimitiveEscape}\left(Gamma,candidate\right)⟺\mathrm{partitionTopology}\left(\mathrm{extendedFamilyReadout}\left(Gamma,candidate\right)\right)<\mathrm{partitionTopology}\left(\mathrm{familyReadout}\left(Gamma\right)\right)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Topology/ObservationEscapeTopology.primitiveEscape_iff_strict_partition_refinement (✓ std3). ∎

Source. Repository-derived.

Commentary.

The complete family readout records every old definition, while the extended readout pairs those coordinates with the candidate value.

Primitive escape is equivalent to strict refinement from the old partition topology to the extended one, with Mathlib’s reversed order on topologies displayed explicitly.

No inhabited-source hypothesis is required. On an empty source, both primitive escape and strict refinement are false, so the biconditional remains valid without asserting an escape.

Theorem 1.2 (Productive separation is a topological target split).

$$\begin{array}{c}\forall X,Current,InputOutput,Target,Output:\mathrm{Type},\\ Gamma:\mathrm{Set}\left(\mathrm{Concept}\left(X,InputOutput\right)\right),\\ current:\mathrm{Concept}\left(X,Current\right),\\ target:\mathrm{Concept}\left(X,Target\right),\\ candidate:\mathrm{Concept}\left(X,Output\right),\\ (\mathrm{ProductiveSeparation}\left(Gamma,current,target,candidate\right)⟺\\ (\exists left,right:X,\mathrm{Inseparable}\left(\mathrm{partitionTopology}\left(current\right),left,right\right)\wedge \\ \neg \mathrm{Inseparable}\left(\mathrm{partitionTopology}\left(target\right),left,right\right)\wedge \\ \mathrm{Inseparable}\left(\mathrm{partitionTopology}\left(\mathrm{familyReadout}\left(Gamma\right)\right),left,right\right)\wedge \\ \neg \mathrm{Inseparable}\left(\mathrm{partitionTopology}\left(candidate\right),left,right\right))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Topology/ObservationEscapeTopology.productiveSeparation_iff_topological_target_split (✓ std3). ∎

Source. Repository-derived.

Commentary.

A productive separation is witnessed by two source states that the current readout cannot separate but the target can.

The same states remain inseparable under the joint readout of the complete old family, while the candidate partition topology separates them.

The biconditional packages exactly these four inseparability and separation clauses. It adds no inhabitedness, finiteness, or continuity hypothesis.

References

• Truth anchor: D5/S3/ConceptDynamics/Topology/ObservationEscapeTopology.primitiveEscape_iff_strict_partition_refinement
• Truth anchor: D5/S3/ConceptDynamics/Topology/ObservationEscapeTopology.productiveSeparation_iff_topological_target_split
• Dependency: D5/S3/ConceptDynamics/DefinitionEscape/DefinitionKernelGalois
• Dependency: D5/S3/ConceptDynamics/ObservationTopology/PartitionTopologyKernel
• Dependency: D5/S3/ConceptDynamics/ObservationTopology/PrimitiveEscapeStrictRefinement
• Dependency: D5/S3/ConceptDynamics/ObservationTopology/ResidualSeparationTopology
• Dependency: D5/S3/ConceptDynamics/ObservationTopology/SemanticClosureTopologyInvariance
• Dependency: D5/S3/ConceptDynamics/ObservationTopology/TargetContinuityFactorization