A.6.4:4.1 - Informal definition
Definition. An EntityOfConcern-retargeting morphism is a local
EpMorphism r : X -> Ywhose exact endpoint epistemes concern different exact entities. A separate bounded-use assertion q affirms or denies that one declared invariant makes the stated loss acceptable for one named receiving use under named conditions.
EntityOfConcernRetargetingMorphism is a local mathematical subtype in the selected formal substrate, not a durable kind. This pattern defines that subtype and the practical discipline for claims about its use.
Keep four things distinct:
- The arrow
r. Within the selected formal substrate, its exact domain X, codomain Y, arrow rule or designator, and declared formal equivalence identify it. The two endpoint epistemes and their different EntitiesOfConcern are recoverable. A changed use claim does not create another arrow. - The bounded-use assertion
q. This is a C.2.1 episteme about exact arrow r. Its ClaimGraph states the invariant, visible loss, named receiving use, conditions, and affirmative or negative polarity. Its complete claim content, exact EntityOfConcern, and effective ReferenceScheme identify q. A citation inside q can point to case facts; it does not decide whether those facts satisfy the proposition. - The current-case judgement. Compare the exact current facts with q’s conditions and proposition, and report
satisfies,fails, orcannot decide. That result is not q’s polarity and does not reidentify q or r. Use A.20 only when the case raises an internal-constraint check, A.10 only for a current evidence-use claim, and B.3 only for a current assurance claim or its material-reliance threshold. Otherwise the named rule and direct case facts are enough. - Any application occurrence. If a system actually computes, authors, or otherwise produces or changes an episteme by using the declared operation, identify that A.6.1 application, its argument and result bindings, the performing system, and any Work separately. The mathematical statement
r : X -> Yalone names no occurrence.
The smallest useful practitioner account still asks six questions:
| Question | What it recovers |
|---|---|
| Which exact arrow relates the source and receiving epistemes? | r’s exact endpoints X and Y, arrow rule or designator, and selected formal substrate’s equivalence criterion |
| Which different entities do they concern? | the independently identified EntityOfConcern pair |
| What exactly does q affirm or deny? | invariant, visible loss, named receiving use, conditions, and polarity |
| Which current facts bear on that proposition? | the direct case basis |
| What do those facts show? | satisfies, fails, or cannot decide |
| If the case cannot be decided, what is missing? | the exact missing fact and reopen condition |
These answers may be one short paragraph; they require no new record form or assurance package. Add a separately governed commitment change, neighboring claim, or durable result only when it changes q, the judgement, or the receiving action; ER-1 and CC-A.6.4-5 name the values to inspect. Add an F.9 Bridge only when the same case separately claims a semantic relation between two exact F.17 local senses.
When the judgement of an affirmative q is fails, retain q as the stated proposition but do not admit that case. When a current-case judgement is cannot decide, keep the source material, name the exact missing fact and what would reopen the question, and stop. Failure of an affirmative q does not by itself establish a negative q; a negative assertion needs its own claim content and case basis.