A.6.2:5 - Archetypal Grounding (Tell–Show–Show)

The examples below show how EFEM is intended to be used across the EntityOfConcern and Description-episteme boundary, specification-use refinements, and Viewpoint/MVPK publication lanes.

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.

A.6.2:5.2 - Internal normalisation of a View (species of EFEM, entityOfConcernChangeMode = preserve)

Context. In MVPK you compute an engineering view V of a system description; you then normalise the view (sort, factor, put equations into normal form) without changing what it says.

Let X = V_raw, Y = V_norm. For this example, assume each episteme independently satisfies E.17.0’s U.View membership condition. The two views have the same:

• entityOfConcernRef(X) = entityOfConcernRef(Y) (same system);
• when grounding is current, the same exact grounding occurrence and grounding holon are found on both sides; this is an endpoint comparison, not a change made by NormalizeView;
• any viewpoint selected by the named normalization use is the same exact P for X and Y; this selection is outside episteme identity;
• representationSchemeRef(X) = representationSchemeRef(Y) (same notation).

The EFEM NormalizeView : X→Y:

• has entityOfConcernChangeMode(NormalizeView) = preserve;
• has a source-to-receiving ClaimGraph difference consisting only of the declared normalization. If an exact EpistemeEditionRelation or another neighboring relation matters, name its predicate and participants on each side and compare the endpoint facts; NormalizeView does not change that occurrence. An assertion such as “normalised at edition E” is part of Y’s ClaimGraph and must pass P2;
• is effect-free. A repeat check uses the next normalization arrow n_Y : Y -> Z under the fixed scheme and normalization rules. It must establish Z = Y under C.2.1 and compose(n_Y, NormalizeView) ≃ NormalizeView under the substrate’s declared arrow equivalence, with a fixture or proof. In the identity fixture, the rule leaves already normalized Y unchanged and uses n_Y = id_Y; P3 then gives compose(n_Y, NormalizeView) = NormalizeView. The exact NormalizeView : X -> Y is self-composable only when X = Y (P3-P4);
• is conservative (P2): no new claims, only re‑expression.

MVPK can reuse the EFEM laws for these normalization arrows. Claim the relevant category and functor only when their mappings, identity laws and composition conditions are established under P3 and the selected MVPK profile.

A.6.2:5.3 - Retargeting sketch (entityOfConcernChangeMode = retarget)

Context. E.18 structural reinterpretation relates a physical-layout episteme to a functional-behaviour episteme. The EntityOfConcern changes from the physical assembly to the functional network.

Inside EFEM, this becomes a species with entityOfConcernChangeMode = retarget:

• input episteme describes S₁ (e.g. a component hierarchy holon);
• output episteme describes S₂ (e.g. a functional network holon);
• one exact arrow r relates the two endpoint epistemes under its declared formal rule; a separate A.6.4 assertion q states the invariant, visible loss, bounded receiving use, conditions, and polarity; and a current-case judgement separately tests the exact facts;
• P2 checks only the formal consequence relation declared for r; the ordinary current-case judgement tests the exact facts against q, and A.20 enters only when that proposition is an internal constraint.

The details belong to A.6.4 and E.18; EFEM provides the generic discipline.

A.6.2:5.4 - Worked endpoint-value and relation-read profile (engineering SystemDescription episteme kind)

(informative)

To make the C.2.1 value and EFEM law discipline concrete, consider an engineering episteme of a dependent system-description kind whose exact EntityOfConcern is one U.System:

This table names the three values that identify an episteme; it is not a RelationSignature or SlotSpec table. EntityOfConcernSlot, ClaimGraphSlot, and ReferenceSchemeSlot are declaration-local SlotKinds only when the reusable C.2.1 EpistemeConstitutionRelationSignature is being inspected. An EFEM species states how the endpoint values compare. If its rule uses a selected viewpoint, empirical-grounding relation, or representation relation, it names the exact occurrence or use qualification separately and reads or compares the endpoint facts without changing the occurrence.

Two typical EFEM species over this kind are:

• Specify_DescEp_SpecDesc_Sys : SystemDescription → SystemSpec — an EntityOfConcernChangeMode = preserve species that:

  • relates independently identified source and receiving epistemes with the same exact EntityOfConcern, makes their effective ReferenceSchemes explicit, and cites any separately obtaining empirical-grounding relation or viewpoint selection only when the formal relation depends on it;
  • satisfies P2 only when every claim in the receiving specification is recoverable from exact source ClaimGraphs or independently current facts under named relations and schemes; the unchanged EntityOfConcern is an endpoint identity condition, not a proposition or additional premise;
  • satisfies C.2.1:7.1 by declaring its endpoint-value comparison, named relation-read profile, and change mode.

• Normalize_EngView — a family of view-normalisation EFEM arrows n_X : X -> Y between exact U.View epistemes (again with EntityOfConcernChangeMode = preserve) that:

  • states how the formal relation uses the three C.2.1 identity values and makes the exact source-to-receiving ClaimGraph difference explicit; any difference between separately obtaining endpoint facts that it compares is named by the exact predicate and participants, and any normalization application remains separate;
  • is effect-free. A repeat claim identifies the next arrow n_Y : Y -> Z under the same rules, establishes Z = Y under C.2.1, and witnesses compose(n_Y, n_X) ≃ n_X under the declared arrow equivalence, as in §5.2;
  • is conservative (P2) by construction: it never introduces new atoms about the selected system.

Concrete A.6.3/A.6.4/E.17.* patterns for engineering description and specification-use idioms state explicitly, under C.2.1:7.1 and CC-EFEM.*, which of the three C.2.1 endpoint values remain the same or differ and which exact separately obtaining relation occurrences their arrow rules read or compare.