Refinement Factorization Category

Abstract

Refinement factorization composes, is reflexive, and has preorder and category readings.

Theorem 1.1 (Refinement factorization composes and supports both readings).

$$\forall X,Btwo,Bone,Bzero:\mathrm{Type},qTwo,qOne,qZero:\mathrm{Concept}(X,Bzero),(\mathrm{Nonempty}(\mathrm{Refines}(qZero,qZero))\wedge (\mathrm{Nonempty}(\mathrm{Refines}(qOne,qZero))\Rightarrow \mathrm{Nonempty}(\mathrm{Refines}(qTwo,qOne))\Rightarrow \mathrm{Nonempty}(\mathrm{Refines}(qTwo,qZero))))\wedge \mathrm{Nonempty}(\mathrm{PreorderWitness}(\mathrm{QuotientCodomainClass}(X)))\wedge \mathrm{Nonempty}(\mathrm{FactorizationCategoryReading}(X)).$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Refinement/FactorizationCategory.refinement_factorization_structure (✓ std3). ∎

Source. Repository-derived.

Commentary.

A refinement is the source factorization data itself: a map from the finer readout codomain to the coarser codomain together with a pointwise commuting equality. The identity map supplies reflexivity, and composing the two factor maps supplies transitivity.

Readouts are constructed from their actual source and codomain types. The quotient carrier identifies readouts exactly when a codomain isomorphism carries one readout to the other; refinement is transported across those representatives, yielding the stated preorder relation.

Without quotienting, the same factorization data forms a category: the public structure includes identities, composition, both identity laws, and associativity. Repository search found no exact theorem packaging all of these clauses; the canonical Concept readout carrier is imported directly.

References

• Truth anchor: D5/S3/ObserverMemory/Refinement/FactorizationCategory.refinement_factorization_structure
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition