Effect-free episteme morphing
About this pattern
This is a generated FPF pattern page projected from the published FPF source. It is canonical FPF content for this ID; it is not a FPF Reference product feature page.
How to use this pattern
Read the ID, status, type, and normativity first. Use the content for exact wording, the relations for adjacent concepts, and citations to keep active work grounded without pasting the whole specification.
Status: Stable Type: Definitional pattern
One-line summary. Effect-free episteme morphing (EFEM) is a local mathematical discipline for law-constrained arrows between exact epistemes. It compares what the source and receiving epistemes say, what they concern, and the schemes that make their claims interpretable, then states the allowed ClaimGraph difference. If its rule needs grounding, representation, conformance, or another separately obtaining relation, it names and reads that occurrence without changing it. The declaration, arrow, use claim, operation application, and performed Work remain distinct.
Use this pattern when a project needs to state and reuse a law-constrained mathematical relation between two exact epistemes while keeping that arrow distinct from a claim that it suits one use, an operation application, publication, and performed Work.
What goes wrong if missed. A view, retargeting, refinement, representation change, publication rendering, mechanism application, or work occurrence is treated as the same operation, so the project can no longer tell whether the EntityOfConcern changed or only the episteme changed.
What this buys. EFEM gives one law-constrained episteme-to-episteme morphism discipline with explicit preserve/retarget mode, clear boundaries among actual values, declaration-local participant meanings, and references, plus conservativity and composition conditions.
Placement. After A.6.1 U.Mechanism and before the A.6.3 epistemic-viewing and A.6.4 EntityOfConcern-retargeting branches.
Builds on.
A.6.0 U.Signature for subject, vocabulary, laws, and applicability; A.6.1 U.Mechanism; A.6.5 for declaration-local SlotSpecs; C.2.1 for U.Episteme identity and direct constitution, empirical-grounding, and edition relations; E.10.D2 for the EntityOfConcern, Description-episteme, describing-use, and specification-use boundary; and C.3 plus F.9 for kind-level and exact cross-local reasoning.
Used by. A.6.3 epistemic viewing; A.6.4 EntityOfConcern retargeting; E.17.0 multi-view describing; E.17 (MVPK); and E.18 structural reinterpretation over transformation-flow structure.
EntityOfConcern change-mode discipline. EFEM uses EntityOfConcernChangeMode for the preserve/retarget characteristic over the exact C.2.1 EntityOfConcern designated by entityOfConcernRef. Earlier source-side spellings must be normalized to the EntityOfConcern family before conformant use and do not define a second EntityOfConcern ontology.
Object settlement. EFEM and EpMorphism are local mathematical classes under C.29, not admitted durable U-kinds. U.Episteme is reused from C.2.1. An A.6.0 FormalSubstrate signature that declares EFEM vocabulary and laws is a separate episteme; one arrow, one use-specific assertion about that arrow, any operation application, performed Work, and publication remain separate objects under their direct governors.
FPF repeatedly needs to relate one exact episteme to another, often alongside a separately described operation that produced the receiving episteme:
Relations
Content
Problem frame
FPF repeatedly needs to relate one exact episteme to another, often alongside a separately described operation that produced the receiving episteme:
- turning an informal method description into a more formal specification;
- projecting a large system description into a smaller “for‑safety‑officer” view;
- re‑expressing the same behavioural model in a different calculus or notation;
- relating an analysis about one subsystem to an analysis about another, with a separate claim about invariant, visible loss, bounded use, conditions, support, and polarity.
All of these can be described by episteme-to-episteme mathematical arrows. The arrow relates exact epistemes and states its laws; it does not itself change an episteme, measure, execute, or actuate. Any operation application and Work remain separate.
Without one reusable local discipline for such arrows:
- every family (KD‑CAL, E.18, MVPK, discipline packs) reinvent their own notion of “projection”, “reinterpretation”, or “refinement”;
- laws about which parts of the source and receiving epistemes may differ, and which grounding or reference-plane facts their rules read and compare, fragment across the spec;
- cross‑family reasoning (e.g. “this E.18 structural reinterpretation is a retargeting, not a view”) becomes brittle and ad‑hoc.
Problem
Concretely, without EFEM:
-
No single place for “effect‑free” discipline. The laws for mathematical relations between exact epistemes are otherwise scattered or implicit; any operation application remains separate.
-
EntityOfConcern behaviour is unclear. Some arrow families have endpoint epistemes about the same EntityOfConcern; others have endpoints about independently different entities. Without a common EntityOfConcernChangeMode discipline, a relation that looks like a harmless representation change can hide a different receiving EntityOfConcern.
-
No functorial backbone. MVPK, KD‑CAL, and E.18 all rely on episteme arrows that compose and respect identities, but the conditions for identity, composition, purity, conservativity, formal domain, and any arrow-family repeat law are not formulated once and reused. Different parts of the spec repeat subtly different sets of laws.
-
Slot/Ref confusion. C.2.1 identifies an episteme through exact claim content, one exact EntityOfConcern, and one effective ReferenceScheme. A.6.5 SlotSpecs apply only inside an exact reusable relation declaration. Laws for projection or retargeting that rely on unnamed fields or tuple positions therefore hide which parts of the source and receiving epistemes are being compared and which separately obtaining facts the rule reads.
The result: engineers and tool builders can no longer tell whether a mathematical relation keeps the same EntityOfConcern, identifies a different receiving one, or merely accompanies an operation. When the endpoints concern different entities, they also need a separate claim saying whether the arrow supports one receiving use, with its invariant, visible loss, conditions, support, and polarity.
Forces
-
Epistemic purity vs operational power. Effect-free episteme arrows are useful because their laws can be reasoned about algebraically and composed. If a use needs I/O, solver calls, measurements, or another effect, identify the operation application and Work separately instead of giving that activity to the arrow.
-
Preserve vs retarget. A viewing arrow has endpoint epistemes with the same EntityOfConcern; a retargeting arrow has independently different ones. A separate A.6.4 use assertion states the invariant, visible loss, receiving use, conditions, support, and polarity.
-
Conservativity vs usefulness. EFEM should be conservative: no new commitments about the EntityOfConcern beyond what input epistemes already entail. The receiving ClaimGraph may factor, aggregate, normalize, or re-express source content and may use a different representation when the loss and interpretation rule are explicit. Any operation or Work that produces that receiving episteme remains separate.
-
Locality vs reference planes and Bridges. Epistemes are interpreted on reference planes (C.2.1). When a use relates two exact source-local senses, test the direct F.9 predicate and cite a Bridge only when it obtains; state the bounded-use claim and any reliance separately. When a use crosses a ReferencePlane, cite its applicable plane relation. EFEM cannot hide either relation inside a “pure” content rewrite, and a local-sense or plane difference alone creates neither one.
-
EntityOfConcern and Description-episteme boundary and specification-use refinement. The EntityOfConcern is not identical to the Description episteme produced by this use; it may itself be
U.Epistemewhen an episteme is under concern....Descriptionnames a Description episteme, and...Specnames one admitted for specification use only when its claims are checkable and the named harness or validation relation can test them. EFEM compares what the two epistemes say, what they concern, and their effective schemes; it states what remains the same and what differs. When grounding or a describing-use viewpoint matters, name the exact relation occurrence or use qualification on each side and compare its facts. The arrow neither changes that occurrence nor establishes viewpoint selection or conformance (A.7, E.10.D2).
Solution — define one local arrow discipline
Informal definition
Definition. An effect-free episteme morphism is a local mathematical arrow
f : X -> Ybetween two exact epistemes. Under its selected formal substrate, it states how claim content, the EntityOfConcern, and any material reference or representation scheme correspond. The arrow itself performs no Work, runs no mechanism, and creates no episteme.
This is a local mathematical class under C.29, not an admitted durable U-kind. The pattern keeps the short name EFEM for that class. A reusable A.6.0 FormalSubstrate signature may declare its vocabulary and P0-P5 laws, but that signature episteme is not the class and is not one arrow.
An arrow in this class:
- has exact domain and codomain epistemes identified under C.2.1;
- is effect-free: no Work, mechanism application, system change, or carrier mutation follows from the arrow;
- states the exact conservativity rule it claims;
- obeys the declared identity and composition laws; and
- declares the local two-value characteristic
EntityOfConcernChangeModeaspreserveorretarget.
Within the selected formal substrate, one arrow is identified by its exact domain, codomain, arrow rule or designator, and declared formal equivalence. Two arrows can have the same endpoints and still be different. Changing a claim about whether the same arrow is suitable for another use does not reidentify the arrow.
The ordinary FPF objects remain separate:
fis the local mathematical arrow;- the A.6.0 FormalSubstrate signature is a C.2.1 episteme declaring reusable vocabulary and laws for the arrow family;
- a C.2.1 assertion about the suitability of
ffor one use is another episteme whose claim content names that use, its conditions, and its polarity; - an operation application and any Work that computes, authors, or changes an episteme are identified only when they actually occur.
The A.6.3 viewing branch has endpoint epistemes about the same EntityOfConcern. The A.6.4 retargeting branch has endpoints about independently different entities; a separate use assertion states the invariant, visible loss, receiving use, conditions, support, and polarity.
Direct signature components (A.6.0 alignment)
When repeated use needs a reusable formal declaration, an A.6.0 U.Signature(profile=FormalSubstrate) episteme may declare this local arrow family. Its direct declaration components are:
SubjectKind here is a type inside the selected formal substrate, not a durable FPF U-kind. Add SliceSet and ExtentRule only if one declared local type genuinely has slice-varying membership; do not use them to hide a use-specific suitability claim.
Vocabulary.
U.Episteme— the exact domain and codomain values.EpMorphism— the local formal type of arrows in the selected substrate.EntityOfConcernChangeMode = {preserve, retarget}— a local two-value characteristic of one arrow, derived from its resolved endpoint EntitiesOfConcern rather than a durable U-kind.Ep— the selected category whose objects are the admitted exact epistemes and whose arrows are the admittedEpMorphismvalues. Call it a category only when it contains the required identities and is closed under every declared composition.EoCBase— the endpoint-only thin category used to compare EntityOfConcern identity. Its objects are the exact independently resolved EntitiesOfConcern represented in the substrate. Between every ordered pair of admitted objectsA,Bit has one formal endpoint arrowu_{A,B};u_{A,A}is the identity, and composition follows endpoints. These arrows are not independently meaningful domain or world-side relations.dom(f)andcod(f)— the exact endpoint epistemes;id_Xandcompose(g,f)— the declared identity and composition operations.α : Ep -> EoCBase— the declared mapping on objects and arrows.α(X)is X's exact EntityOfConcern afterentityOfConcernRef(X)resolves it. Forf : X -> Y,α(f)is the unique endpoint arrowu_{α(X),α(Y)}. It deliberately forgets f's arrow rule; different Ep arrows with the same endpoint EntitiesOfConcern therefore have the same image. For each arrow, recover the C.2.1 identity values of X and Y and state which identity-bearing values or ClaimGraph parts are preserved or differ. If the arrow rule uses a neighboring relation, name its exact predicate and participants on each side and state which endpoint facts it reads or compares. Equal or different endpoint profiles do not mean that the arrow changed a relation occurrence or made it obtain or cease; any actual relation change and producing application or Work remain under their direct patterns.SubjectRefremains only a legacy source projection; resolve it to the exact episteme and EntityOfConcern.
A claim that f is suitable for one exact use is a separate C.2.1 assertion. An actual operation application has its own declared argument and result bindings under A.6.1, and any system that performs it and any resulting Work remain under their direct patterns. Neither the signature nor the mathematical statement f : X -> Y supplies that occurrence.
Laws and applicability. P0-P5 below govern the local arrow class. A.6.5 SlotSpecs enter only when an exact reusable direct-relation declaration is current; they are not fields of X, Y, or f.
Laws P0–P5 (normative)
All laws below test membership in the local EFEM arrow class under the selected formal substrate. They do not assert membership in a durable U-kind.
P0 — Typed episteme, endpoint-value, and relation-read profile (C.2.1-grounded)
For any arrow f : X→Y presented as an effect-free episteme morphism:
-
Typed epistemes.
XandYare epistemes of declared kindsK_X, K_Y : U.EpistemeKind, each identified under C.2.1 by exact claim content, one EntityOfConcern, and one effective ReferenceScheme. Grounding and representation relations are added only when current; a viewpoint selected for a named describing use remains outside episteme identity. -
Value and use projection. For each episteme
E—and separately for a named describing use when one is current—EFEM laws may refer to:content(E) : U.ClaimGraph— E's exact identity-bearing claim content;entityOfConcernRef(E) : U.EntityRef— designates E's exact EntityOfConcern;selectedViewpointRef?(use) : U.ViewpointRef— only when the named describing use selects one exact viewpoint; this is not a component of E's identity;referenceScheme?(E) : U.ReferenceScheme— E's effective designation and interpretation scheme;representationSchemeRef?(E) : U.RepresentationSchemeRef— only when an exact C.29 representation scheme and correspondence relation are current for E; this is not a C.2.1 identity component;- a separately current neighboring fact — name the exact
EpistemeEditionRelation, exact A.10 evidence or provenance relation, or other governed predicate and its participants when the arrow family reads or compares it; do not collect these facts in a generic projection. If E asserts such a fact, that assertion is already part ofcontent(E).
When grounding matters, name the exact grounding relation, its grounding holon, and the claims it covers; grounding is not another component of episteme identity.
-
Derived
EntityOfConcernChangeModeand subtype restriction. Each admitted arrow receives its mode from its resolved endpoint EntitiesOfConcern:entityOfConcernChangeMode(f) = preservewhen X and Y concern the same exact entity; a current grounding relation remains a separately governed fact;entityOfConcernChangeMode(f) = retargetwhen X and Y concern independently different entities. Any claim that f supports one receiving use is a separate A.6.4 assertionqwith its own invariant, visible loss, receiving use, conditions, support, and polarity.
The parent EFEM class contains both modes. A named species or subtype may admit only one mode, but that restriction does not by itself make the subtype closed under composition. Classify each composite again from its final endpoints under P3.
-
Legacy SubjectRef and describing-use discipline. For Description epistemes, including those admitted for specification use, resolve legacy
subjectRef(E)to exact E and its EntityOfConcern. State which endpoint claim content, EntityOfConcern, and effective scheme are preserved or differ. When grounding or a selected describing-use viewpoint matters, name the exact occurrence or use qualification on each side and state which facts the rule reads or compares. The morphism changes no such occurrence; viewpoint selection is neither identity nor conformance.
P1 — Effect-free arrow, separate execution
The mathematical statement f : X -> Y neither changes a system nor says that a system computed, authored, stored, transmitted, or published Y.
When a system actually measures, simulates, translates, normalizes, fits, or otherwise produces or changes an episteme, identify separately:
- the exact A.6.1 operation application and its argument and result bindings, when that declaration is current;
- the system and any performed Work;
- the affected or newly constituted episteme and its C.2.1 identity facts; and
- any production, evidence, publication, or reliance relation that actually obtains under its own direct governor.
The same arrow can relate already existing epistemes, or be used in several separately identified applications. Conversely, two applications do not become the same because they use the same arrow. No bare result or universal production relation follows from the arrow or its declaration.
P2 — Claim conservativity (no unlicensed commitments)
Let content_X = content(X) and content_Y = content(Y), with their effective ReferenceSchemes and exact EntitiesOfConcern. Interpret each ClaimGraph through its effective scheme. Name any additional exact source episteme, current fact, grounding relation, or scheme correspondence that the arrow rule actually admits; an entity or label by itself is not a claim premise. Then:
Every assertion in
content_Ymust be recoverable as a logical consequence, conservative re-expression, selection, or declared aggregation of the identified source ClaimGraphs and exact admitted facts under the named schemes. This includes assertions about an episteme's edition, source, status, witness, provenance, or evidence. Calling an assertion metadata does not exempt it from P2.
An EFEM arrow may omit claims or conservatively reorganize and re-express them. It may not introduce an unsupported atomic commitment, silently widen claim scope, or cross a ReferencePlane without the exact relation required for that move.
A separately obtaining edition, provenance, evidence, or status relation remains outside episteme identity. If the arrow family compares such a relation across X and Y, name the exact predicate and participants on each side. The arrow records that comparison; it does not create or update the relation. If Y asserts the relation, that assertion is identity-bearing content_Y and must pass the same source-to-result trace as every other assertion.
Where entityOfConcernChangeMode(f) = retarget, the arrow declaration states its formal cross-entity correspondence; it does not itself establish conservativity for a receiving use. A separate A.6.4 assertion states the invariant, visible loss, bounded use, conditions, support, and polarity for that use. An ordinary time-to-frequency representation of the same signal instead routes through C.29 and A.6.3.RT. A Fourier relation enters a retargeting case only after C.2.1 independently identifies a different receiving EntityOfConcern.
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.
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: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: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. A separate assertion says whether the composite suits one final receiving use and states its invariant, accumulated visible loss, conditions, support, and polarity.
-
Scheme-aware composition. If endpoint RepresentationSchemes or effective ReferenceSchemes differ, name the exact C.29 or A.6.3.RT correspondence used by each route and state the equality or declared equivalence that makes the two routes agree. 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.
P4 — Arrow and repeat boundary
The common EFEM model treats f : X -> Y as one arrow with exact endpoints, an arrow rule or designator, and declared formal equivalence. It does not treat every arrow as a function that can be evaluated on an object, and it makes no claim that a separately declared operation is deterministic. A concrete substrate may add an evaluation operation only after declaring its argument kind, result kind, and relation to these exact arrows; that extra operation is not part of the common EFEM laws.
No universal idempotence follows. A normalization or another endomorphism f : X -> X may separately claim a repeat law such as compose(f,f) ≃ f only when composition is defined on the declared domain, ≃ is the substrate's stated equivalence, and a working fixture or proof supplies the witness. This mathematical repeat claim is not evidence that an operation was executed twice.
P5 — Formal domain and separate use conditions
Each arrow family states the formal domain in which its laws apply:
- the allowed kinds of the two exact endpoint EntitiesOfConcern;
- any exact grounding relations or endpoint facts that the arrow rule reads;
- the admitted RepresentationScheme and ReferenceScheme pairs and any C.29 or A.6.3.RT correspondence needed by the formal relation; and
- any ClaimScope constraint required by the arrow law itself.
If X or Y lies outside that domain, the arrow is not a member of this local family. This is distinct from an operation application being admitted or rejected. A use-specific scope, operating condition, selected viewpoint, invariant, visible loss, support, and polarity belong in the separate use assertion when they decide whether one arrow supports one receiving use; changing that assertion does not reidentify the arrow.
When the use also relates two exact F.17 local senses and the F.9 predicate obtains, cite that Bridge and a separate bounded-use claim. When it crosses a ReferencePlane, cite the applicable plane relation. If transport is performed, identify the A.6.1 application separately. Different labels, contexts, schemes, planes, or operating conditions alone create none of these relations.
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.
Typed specification-use refinement SpecifyDescEpSpecDesc (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.MethodDescriptionepisteme withentityOfConcernRef(X) : U.MethodRef,content(X) : U.ClaimGraph_D, andReferenceScheme_D; when the named engineering validation use selects viewpoint P, record that selection separately. - Codomain:
Y = U.MethodSpecepisteme with the sameentityOfConcernRef(Y) = entityOfConcernRef(X), more structuredcontent(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, and applicability is bounded by the named engineering scope, operating conditions, effective scheme, and any viewpoint selected for the named validation use.
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 an operation application or performed Work produced that strengthening, identify it separately; neither the new assertion nor its production becomes part of a conservative arrow.
This matches A.7 and E.10.D2: an EntityOfConcern and a Description episteme about it remain distinct. C.2.1 identifies the episteme by its complete claim content, exact EntityOfConcern, and effective ReferenceScheme; when a describing use or production relation matters, name that exact relation separately. This account needs no universal EntityOfConcern -> Description function and is not itself an episteme-to-episteme morphism. Specify_DescEp_SpecDesc is an optional EFEM species over a Description episteme after a specification-use or refinement gate is present. EFEM supplies only the conservative episteme-to-episteme laws; it does not grant specification use or make Specification a third peer in A.7.
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, both U.EpistemeView instances with 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
EpistemeEditionRelationor another neighboring relation matters, name its predicate and participants on each side and compare the endpoint facts;NormalizeViewdoes 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 and separately claims idempotence on the output-closed domain of valid
EpistemeViewvalues under the fixed scheme and normalization rules; equality means exact normalized ClaimGraph equality plus equality of all identity-bearing episteme values, and a fixture that composesNormalizeViewwith itself supplies the repeat witness (P4); - is conservative (P2): no new claims, only re‑expression.
MVPK can then assume functoriality of such normalisations without re‑stating the EFEM laws.
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
rrelates the two endpoint epistemes under its declared formal rule, while a separate A.6.4 assertionqstates the invariant, visible loss, bounded receiving use, conditions, support, and polarity; - P2 checks only the formal consequence relation declared for
r; any A.20 check onqevaluates the exact proposition in that separate assertion.
The details belong to A.6.4 and E.18; EFEM provides the generic discipline.
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— anEntityOfConcernChangeMode = preservespecies 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 : EpistemeView → EpistemeView— a view‑normalisation EFEM (again withEntityOfConcernChangeMode = 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 and separately claims idempotence on its output-closed engineering-view domain under the fixed scheme and normalization rules; equality means exact normalized ClaimGraph equality plus equality of all identity-bearing episteme values, and a composition fixture supplies the repeat witness (P4);
- 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.
Bias-Annotation
-
Episteme‑first, world‑second. EFEM is strictly about epistemes as objects; any world contact (measurements, executions) lives in
U.Mechanism/U.Workand produces new epistemes that EFEM may subsequently relate. -
Actual values, not unnamed fields. Laws name the exact claim content, EntityOfConcern, and effective ReferenceScheme they use and keep empirical grounding, representation, view conformance, and describing-use viewpoint selection separate. A SlotKind is mentioned only when the exact reusable relation declaration is current.
-
Arrow domain and use-local semantics. EFEM names the formal domain of each arrow family. A separate use assertion carries any use-specific scope, operating conditions, selected viewpoint, invariant, visible loss, support, and polarity. An obtaining semantic Bridge between two exact local senses, a ReferencePlane relation, and any transport application remain separately identified; no implicit cross-local or cross-plane EFEM is permitted.
-
EntityOfConcern and Description-episteme boundary and specification-use/refinement respect. EFEM never collapses an EntityOfConcern with a Description episteme or with a specification-use refinement. C.2.1 identifies each Description episteme directly; any authoring, measurement, observation, model, source-use, representation, or refinement relation is stated only when it is current. A specification refinement can be represented by an EFEM arrow only after an exact specification-use or refinement gate admits it; any application that produces the refined episteme remains separate.
Conformance Checklist (normative)
Common Anti-Patterns and How to Avoid Them
Consequences
-
Single place for episteme‑to‑episteme laws. Effect-free arrow families used across KD‑CAL, MVPK, E.18, and discipline packs can reuse one local law set instead of re-inventing it. Each actual application and use claim remains separate.
-
Clear separation from mechanisms & work. Anything that touches the world, including measurement, execution, or simulation, belongs to the applicable
U.Mechanismapplication or performedU.Work; EFEM remains effect-free and compositional. Any semantic correspondence, temporal qualification, evidence, or reliance claim remains under its own pattern. -
Stable backbone for Viewing & Retargeting. A.6.3 and A.6.4 do not need to repeat P0–P5; they specialise EFEM with additional constraints (preserve/retarget). Other patterns (e.g. MultiViewDescribing, MVPK, E.18 structural reinterpretation) can depend on EFEM as a stable base.
-
Value-and-relation clarity. By requiring each EFEM species to compare the three C.2.1 identity values and name the exact separately obtaining relations its rule reads, the pattern keeps an EntityOfConcern, a declaration-local SlotKind, and a reference to the entity distinct. Equal or different endpoint relation facts are a comparison result, not an effect of the arrow.
-
Better didactics. The traditional “semantic triangle” becomes a didactic projection over C.2.1 episteme constitution and the neighboring relations an EFEM species actually uses. It can gesture at expression, meaning, and subject without turning viewpoint, empirical grounding, representation, or reference into one slot tuple.
Rationale
Why a separate EFEM pattern (A.6.2) instead of folding into A.6.1 or C.2.1?
- A.6.1 defines Mechanism declarations and their separately identified applications, including operational guards and time conditions. A.6.2 instead defines a local mathematical arrow class. Any semantic Bridge, plane relation, transport application, or Work remains under its direct pattern.
- C.2.1 fixes episteme identity through claim content, exact EntityOfConcern, and effective ReferenceScheme and keeps neighboring direct relations separate, but does not define morphisms. EFEM is a morphism-level pattern over those values and relations.
This split mirrors how A.6.0 separates a declaration from what later uses it: C.2.1 says what an episteme is; A.6.2 states the laws of a local episteme-to-episteme arrow family; A.6.1 and A.15 govern any application and Work.
Why insist on EntityOfConcernChangeMode?
Because a relation can look like a harmless view even though its endpoint epistemes concern different entities—for example, component assembly and function bundle. Declaring preserve versus retarget exposes that endpoint distinction. It does not make the arrow fit for a use; the separate assertion must state the invariant, visible loss, bounded use, conditions, support, and polarity.
Why name actual values and exact relation reads instead of informal fields?
FPF distinguishes actual participants and their references from the declaration-local SlotKinds used in a reusable RelationSignature. Reusing that distinction here:
- aligns episteme morphisms with the framework's direct-relation architecture;
- enables checks that an EFEM species compared only the three declared endpoint values, read only the named neighboring occurrences, and left any actual relation change to its direct pattern and producing application or Work;
- avoids minting another generic parameter, field, or relation-role vocabulary.
SoTA-Echoing
Practice question. What current transformation practice supports reusable definitions and composition while keeping execution and correctness evidence separate, and does it justify a universal repeat law?
The thin EFEM arrow class is a bounded FPF synthesis. Reopen it if a current transformation practice needs a different arrow identity or effect boundary, or if a concrete composition cannot be stated without collapsing the declaration, application, or correctness claim.
Relations
-
Specialises / is specialised by.
- Builds on A.6.0
U.Signaturefor direct subject, range, optional result, slice, and extent components together with Vocabulary, Laws, and Applicability; coordinates with A.6.1U.Mechanismwithout making mechanism application part of EFEM. - Refined by the A.6.3 EntityOfConcern-preserving viewing branch and the A.6.4 EntityOfConcern-retargeting branch.
- Builds on A.6.0
-
Constrained by. A.6.5 declaration-local SlotSpec discipline; C.2.1 episteme constitution and any separately current empirical-grounding or edition relation; E.10.D2 for the EntityOfConcern, Description-episteme, describing-use, and specification-use boundary; Part F for exact local-sense or ReferencePlane relations; and E.10 for naming discipline.
-
Consumed by. E.17.0
U.MultiViewDescribing(families of Description epistemes, including Description epistemes admitted for specification use, under Viewpoints); E.17 (MVPK — publication as species of Viewing/EFEM); E.18 (structural reinterpretation and other transformation-flow relations over epistemes); KD‑CAL/LOG‑CAL rules that reason about episteme transforms categorically.
A.6.2:End
Last Updated: 2026-08-30 — upstream FPF commit e400eab3 (github.com/ailev/FPF)