Ordinary Readouts Have Single-Stage Representatives

Abstract

Every ordinary readout from a cofiltered stage system is represented by a map from one presentation stage.

Theorem 1.1 (Every ordinary readout has a finite stage).

$$\begin{array}{c}\forall q\in {\mathrm{colim}}_i\mathrm{Hom}(X_i,D),\exists i,q_i:X_i\to D,[q_i]=q,\\ \forall q\in {\mathrm{colim}}_i\mathrm{Hom}(X_i,\mathbb{R}),\exists i,q_i:X_i\to \mathbb{R},[q_i]=q,\\ \forall q\in {\mathrm{colim}}_i\mathrm{Hom}(X_i,\mathbb{C}),\exists i,q_i:X_i\to \mathbb{C},[q_i]=q.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/ProObjects/FiniteStageReadout.every_ordinary_readout_has_finite_stage (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let I be a small cofiltered category, let X : I -> C be a stage diagram, and let D be an ordinary target object. Stage readouts form a functor on the opposite index category: a refinement map transports a readout by precomposition. An ordinary readout is constructed as the standard colimit quotient of these stage hom-sets.

Every element of that colimit quotient is represented by one pair consisting of an index i and a morphism X_i -> D. This is the formal content of needing one sufficiently refined presentation stage rather than a simultaneous compatible family of readouts at every stage.

The public theorem states the generic categorical clause and, as separate conjuncts, the real- and complex-valued clauses for type-valued stage systems. No discreteness or finiteness condition is placed on the real or complex target; finite-stage refers to presentation through one stage, not to the target’s cardinality.

Pinned Mathlib has no matching pro-category API. Its concrete colimit type is the quotient of the disjoint union of component values by the relation generated by transition maps, and the exact theorem Functor.ιColimitType_jointly_surjective is applied directly to obtain the representative.

References

• Truth anchor: D5/S3/ObserverMemory/ProObjects/FiniteStageReadout.every_ordinary_readout_has_finite_stage