A.6.2:5.1 - Typed specification-use refinement Specify_DescEp_SpecDesc (species of EFEM)

Context. You have a U.MethodDescription for a safety check and want a more formal U.MethodSpec with checkable constraints or test-harness obligations about the same Method. Before calling the relation conservative, identify the exact claims that already support those constraints.

Shape.

• Domain: X = U.MethodDescription episteme with entityOfConcernRef(X) : U.MethodRef, content(X) : U.ClaimGraph_D, and ReferenceScheme_D; when the named engineering validation use selects viewpoint P, record that selection separately.
• Codomain: Y = U.MethodSpec episteme with the same entityOfConcernRef(Y) = entityOfConcernRef(X), more structured content(Y) : U.ClaimGraph_S, and a more explicit ReferenceScheme. If the same named validation use continues, it preserves its selected viewpoint P separately.

Specify_DescEp_SpecDesc is a species of EFEM only when all of these hold:

• entityOfConcernChangeMode(Specify_DescEp_SpecDesc) = preserve. The shared Method establishes endpoint EntityOfConcern equality; the Method entity itself is not a logical premise.
• P1 — effect-free: it is the declared arrow between the two epistemes; any operation application that produces Y is separate.
• P2 — conservative: every behavioral claim, constraint, and test obligation in Y traces to exact claims in X, an additional named source episteme, or an independently current fact under its named relation and effective scheme.
• P3-P5 — category structure and scope: the declared arrows compose only when their exact endpoints and P3 mappings agree. P5 includes the named engineering scope, operating conditions, effective scheme, or selected viewpoint in the formal domain only insofar as the arrow law depends on them. Keep separately any such condition or viewpoint that changes the named validation or receiving-use claim.

If an author chooses a new threshold, acceptance condition, harness obligation, or other commitment not supported by that basis, Y has been strengthened and the proposed arrow fails P2. Identify the new assertion in Y’s changed ClaimGraph. When a particular application or Work accounts for that strengthening, identify that occurrence and the direct production relation separately. The new assertion remains outside the conservative arrow; the application, Work, and production relation account for its origin.

Keeping episteme identity, describing use, and production separate matches A.7 and E.10.D2. Under C.2.1, each Description episteme is identified by its complete claim content, its own exact EntityOfConcern reference, and its effective ReferenceScheme; any describing use or production relation is separately identified. Specify_DescEp_SpecDesc is an optional EFEM species once a specification-use or refinement gate admits that use. E.10.D2 governs specification-use admission, A.7 governs the Description/Specification distinction, and the declared Specify_DescEp_SpecDesc arrow carries the episteme-to-episteme relation.