A.6.2:4.3.4 - P3 — Category structure and EntityOfConcern mapping
Use this law only after the selected FormalSubstrate declares both categories and the mapping below. Ep has admitted exact epistemes as objects and admitted EFEM arrows as arrows. It is a category only when it contains the required identities and every composite of admitted arrows with a matching middle episteme. If that closure is absent, keep the individual arrows and do not claim this category or functor.
EoCBase is the endpoint-only thin category over the exact resolved EntitiesOfConcern represented in the substrate. For every admitted pair A,B, it contains one formal arrow u_{A,B}. Its only endomorphism at A is u_{A,A}=id_A, and compose(u_{B,C},u_{A,B})=u_{A,C}. This formal arrow records only endpoint identity or difference; it is not an F.9 Bridge, a domain relation, or a claim that any world-side relation obtains.
α : Ep -> EoCBase
On objects, α(X) is the exact EntityOfConcern resolved through entityOfConcernRef(X); the reference is only the means of resolution. For f : X -> Y, α(f)=u_{α(X),α(Y)}. Thus a preserve-mode arrow maps to the base identity even when f is not an identity arrow in Ep, while a retarget-mode arrow maps to the unique formal arrow between its different endpoint entities. α intentionally forgets the rule that distinguishes two Ep arrows with the same endpoint entities.
Practitioner check. Point to exact X, Y, and f; resolve both EntitiesOfConcern; and identify the resulting endpoint arrow. For a proposed composition, point to the exact middle episteme and the admitted composite, then check P0-P2 for that composite. If the family lacks a required identity or composite, use its individual arrows without claiming the category or functor. No extra proof or record is required unless the receiving use calls for one.
-
Identities. For each admitted episteme X, Ep contains
id_X : X -> X. For everyf : X -> Y:dom(id_X) = X cod(id_X) = X compose(id_Y, f) = f = compose(f, id_X) α(id_X) = id_α(X)id_Xpreserves the episteme’s claim content, EntityOfConcern, effective ReferenceScheme, and every other declared episteme value. A viewpoint selected for one named describing use remains a separate use qualification. -
Composition. For admitted
f : X -> Yandg : Y -> Z, Ep contains an admittedh = compose(g,f) : X -> Z; h must satisfy P0-P2. It also satisfies:dom(h) = X cod(h) = Z α(h) = compose(α(g), α(f)) compose(k, compose(g,f)) = compose(compose(k,g), f)The α equation is replayable from endpoints. For a retargeting round trip from entity A through B back to A, both sides are the unique base endomorphism
u_{A,A}=id_A; this says nothing about inverse world-side relations or identical Ep arrow rules. The composite haspreservemode when X and Z concern the same exact entity andretargetmode when they concern different entities.A preserve-only or retarget-only subtype is not thereby closed under parent composition. A composite remains in that subtype only when its final mode and all additional subtype laws match; otherwise it remains an EFEM arrow in the parent class. When a receiving-use claim is made, a separate
qstates the final-use invariant, accumulated visible loss, receiving use, conditions, and polarity; a separate current-case judgement tests the final facts. -
Scheme-aware composition. If endpoint RepresentationSchemes or effective ReferenceSchemes differ, name the exact correspondence used by each route under its direct governor and state the equality or declared equivalence that makes the two routes agree. A.6.3.RT governs a same-EntityOfConcern representation-scheme transition; C.29 governs any mathematical-lens use. A scheme difference alone establishes neither. Use
natural,oplax, or similar terminology only when the substrate supplies the actual mapping, comparison arrow, diagram, and working probe. Otherwise state the required two-route agreement in ordinary language. Any witness episteme remains separately identified.