Refinement Composition Structure

Abstract

Refinement composes, forms a factorization category, and descends to a preorder.

Theorem 1.1 (Refinement composition, category laws, and quotient preorder).

$$\begin{array}{c}\forall X,BC,BD,BE:\mathrm{Type},\\ C:\mathrm{Concept}\left(X,BC\right),D:\mathrm{Concept}\left(X,BD\right),E:\mathrm{Concept}\left(X,BE\right),\\ (\mathrm{Refines}\left(C,D\right)\Rightarrow \mathrm{Refines}\left(D,E\right)\Rightarrow \mathrm{Refines}\left(C,E\right))\wedge \\ \mathrm{Refines}\left(C,C\right)\wedge \\ ((\forall r:\mathrm{Readout}\left(X\right),\mathrm{identity}\left(\mathrm{fixedCodomainFactorizationCategory}\left(X\right),r\right)=\mathrm{identityRefinement}\left(\mathrm{readout}\left(r\right)\right))\wedge \\ (\forall r0,r1,r2:\mathrm{Readout}\left(X\right),h0:\mathrm{Refines}\left(\mathrm{readout}\left(r0\right),\mathrm{readout}\left(r1\right)\right),h1:\mathrm{Refines}\left(\mathrm{readout}\left(r1\right),\mathrm{readout}\left(r2\right)\right),\mathrm{compose}\left(\mathrm{fixedCodomainFactorizationCategory}\left(X\right),h0,h1\right)=\mathrm{composeRefinement}\left(h1,h0\right))\wedge \\ (\forall r0,r1:\mathrm{Readout}\left(X\right),h:\mathrm{Refines}\left(\mathrm{readout}\left(r0\right),\mathrm{readout}\left(r1\right)\right),\mathrm{compose}\left(\mathrm{fixedCodomainFactorizationCategory}\left(X\right),\mathrm{identity}\left(\mathrm{fixedCodomainFactorizationCategory}\left(X\right),r0\right),h\right)=h)\wedge \\ (\forall r0,r1:\mathrm{Readout}\left(X\right),h:\mathrm{Refines}\left(\mathrm{readout}\left(r0\right),\mathrm{readout}\left(r1\right)\right),\mathrm{compose}\left(\mathrm{fixedCodomainFactorizationCategory}\left(X\right),h,\mathrm{identity}\left(\mathrm{fixedCodomainFactorizationCategory}\left(X\right),r1\right)\right)=h)\wedge \\ (\forall r0,r1,r2,r3:\mathrm{Readout}\left(X\right),h0:\mathrm{Refines}\left(\mathrm{readout}\left(r0\right),\mathrm{readout}\left(r1\right)\right),h1:\mathrm{Refines}\left(\mathrm{readout}\left(r1\right),\mathrm{readout}\left(r2\right)\right),h2:\mathrm{Refines}\left(\mathrm{readout}\left(r2\right),\mathrm{readout}\left(r3\right)\right),\mathrm{compose}\left(\mathrm{fixedCodomainFactorizationCategory}\left(X\right),\mathrm{compose}\left(\mathrm{fixedCodomainFactorizationCategory}\left(X\right),h0,h1\right),h2\right)=\mathrm{compose}\left(\mathrm{fixedCodomainFactorizationCategory}\left(X\right),h0,\mathrm{compose}\left(\mathrm{fixedCodomainFactorizationCategory}\left(X\right),h1,h2\right)\right)))\wedge \\ ((\forall A,B:\mathrm{Readout}\left(X\right),\mathrm{toAntisymmetrization}\left((P,Q:\mathrm{Readout}\left(X\right)\mapsto P\le Q),A\right)\le \mathrm{toAntisymmetrization}\left((P,Q:\mathrm{Readout}\left(X\right)\mapsto P\le Q),B\right)⟺\mathrm{Refines}\left(\mathrm{readout}\left(A\right),\mathrm{readout}\left(B\right)\right))\wedge \\ (\forall left:\mathrm{ReadoutRefinementClass}\left(X\right),left\le left)\wedge \\ (\forall left,middle,right:\mathrm{ReadoutRefinementClass}\left(X\right),left\le middle\Rightarrow middle\le right\Rightarrow left\le right)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/RefinementFactorization/RefinementCompositionStructure.refinement_composition_category_and_quotient_preorder (✓ std3). ∎

Source. Repository-derived.

Commentary.

Canonical refinement is factorization of one concept readout through another. Existing family theorems supply transitivity by composition and reflexivity by the identity map.

The named factorization-category object uses those source maps as its morphisms. The public statement exposes its identity and composition computations together with both unit laws and associativity.

All bundled concept readouts are quotiented by mutual refinement through Mathlib antisymmetrization. The quotient order is identified publicly with refinement of representatives and is then stated directly to be reflexive and transitive.

References

• Truth anchor: D5/S3/ConceptDynamics/RefinementFactorization/RefinementCompositionStructure.refinement_composition_category_and_quotient_preorder
• Dependency: D5/S3/ConceptDynamics/Refinement/RefinementReflexivity
• Dependency: D5/S3/ConceptDynamics/Refinement/RefinementTransitivity
• Dependency: D5/S3/ObserverMemory/Refinement/FactorizationCategory