Faithful Observation Topology

Abstract

Injective observations induce discrete topology and preserve catalog escapes.

Theorem 1.1 (A readout induces the discrete topology exactly when it is injective).

$$\forall observe:\mathrm{Concept}\left(X,Observation\right),\mathrm{partitionTopology}\left(observe\right)=\mathrm{bottomTopology}\left(X\right)⟺\mathrm{Injective}\left(observe\right).$$

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

Source. Repository-derived.

Commentary.

The partition topology identifies precisely those source points with equal observed values.

If the topology is discrete, inseparable source points are equal, so equal observations force equal inputs. Conversely, an injective readout has the same fibers as the identity.

The biconditional concerns equality with the bottom, hence discrete, topology on the source and adds no inhabitedness assumption.

Theorem 1.2 (Discreteness is preservation of every one-row catalog escape).

$$\begin{array}{c}\forall observe:Output\to Observation,\\ ([\mathrm{Nonempty}\left(Input\right)])\Rightarrow \\ (\mathrm{partitionTopology}\left(observe\right)=\mathrm{bottomTopology}\left(Output\right)⟺(\forall catalog:Unit\to Input\to Output,candidate:Input\to Output,\\ \mathrm{CatalogEscape}\left(catalog,candidate\right)\Rightarrow \\ \mathrm{CatalogEscape}\left(\mathrm{observedCatalog}\left(observe,catalog\right),\mathrm{observedCandidate}\left(observe,candidate\right)\right))).\end{array}$$

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

Source. Repository-derived.

Commentary.

Assume the catalog input type is inhabited. The theorem compares discreteness of the observation partition with a universal one-row escape-preservation law.

For every Unit-indexed catalog and candidate, a genuine escape before observation must remain an escape after both are postcomposed with the observation.

The statement is an exact biconditional. It does not assert the preservation law without the displayed Nonempty instance.

References

• Truth anchor: D5/S3/ConceptDynamics/ObservationTopology/FaithfulObservationTopology.discrete_partition_iff_preserves_unit_catalog_escape
• Truth anchor: D5/S3/ConceptDynamics/ObservationTopology/FaithfulObservationTopology.partitionTopology_eq_discrete_iff_injective
• Dependency: D5/S3/ConceptDynamics/ObservationTopology/EscapeUnderObservation
• Dependency: D5/S3/ConceptDynamics/ObservationTopology/PartitionTopologyKernel