Continuous Refinement Observation Topology

Abstract

A continuous refinement factorization makes every coarse observation-open set open for the refined readout.

Theorem 1.1 (Continuous refinement makes the observation topology finer).

$$\begin{array}{c}\forall X,B,R:\mathrm{Type},\\ [\mathrm{TopologicalSpace}\left(B\right)],[\mathrm{TopologicalSpace}\left(R\right)],\\ C:X\to B,D:X\to R,p:R\to B,\\ (C=p\circ D\wedge \mathrm{Continuous}\left(p\right))\Rightarrow \\ \forall U:\mathrm{Set}\left(X\right),\mathrm{IsOpen}\left(\mathrm{induced}\left(C,\mathrm{topology}\left(B\right)\right),U\right)\Rightarrow \mathrm{IsOpen}\left(\mathrm{induced}\left(D,\mathrm{topology}\left(R\right)\right),U\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

The observation topology of a readout is constructed directly as the topology induced from its value space. No separate observation-topology definition is introduced.

Let the coarse readout factor as a continuous projection after the refined readout. Every subset open for the coarse induced topology is then open for the refined induced topology.

The proof applies the pinned library laws Continuous.le_induced, induced_mono, and induced_compose directly.

References

• Truth anchor: D5/S3/ConceptDynamics/Topology/ContinuousRefinementObservationTopology.continuous_refinement_observation_topology