A.6.3:4 - Solution
Local mantra. Identify X and Y. Hold their EntityOfConcern fixed. State the conservative construction and admitted loss. Add exact correspondence dependencies when used. Test U.View membership separately under E.17.0 only when the receiving use needs that membership.
A.6.3:4.1 - Identify both epistemes independently
Before declaring a viewing, recover for each of X and Y under C.2.1:
- exact claim content;
- exact EntityOfConcern;
- effective
U.ReferenceScheme.
X and Y are separate epistemes whenever one of those identity discriminators differs. A filename, table, diagram, query result, viewpointRef, or publication form is not a substitute for either identity.
If the supposed receiving item has no recoverable claim content or EntityOfConcern, stop: the receiving episteme has not been identified. If the exact EntityOfConcern differs, use A.6.4 retargeting rather than A.6.3.
A.6.3:4.2 - Declare the viewing construction
A.6.3 viewing is the EntityOfConcern-preserving branch of A.6.2’s local effect-free arrow class. In the selected formal substrate, one viewing arrow is written v : X -> Y and has exact source episteme X and exact receiving episteme Y.
The reusable A.6.0 declaration describes the admitted local arrow family, rather than turning one arrow or endpoint pair into a kind:
SubjectKind = local A.6.2 EpMorphism type restricted to preserve-mode viewing arrows
RangedValueKind = admitted ordered-pair range over exact U.Episteme values satisfying the declared endpoint-kind constraints
ResultKind = omitted; v is the declared subject and Y is its exact receiving endpoint
Applicability = selected formal substrate, admitted endpoint kinds, viewing-rule conditions, and preserve mode
EpMorphism is a local mathematical type in the selected substrate, not a durable FPF U-kind. The arrow records the declared construction from X to Y. Section 4.6 separately governs an account of its actual execution.
A concrete viewing declaration states:
- exact X and exact Y;
- that
EntityOfConcern(X)=EntityOfConcern(Y); - the claim-content construction from X and any additional exact sources to Y;
- how the source and receiving reference schemes are related;
- preserved claim components, admitted omissions or losses, and prohibited strengthening;
- applicability conditions and any fixed configuration needed for replay.
A separate assertion says whether this arrow supports one named receiving use and states any use-specific loss or conditions. If the current use needs an account of a query, rewrite, model, or other method being applied, identify that application and any admitted Work separately; v : X -> Y alone does not assert that they occurred.
A.6.3:4.3 - Apply the same-EntityOfConcern and conservativity laws
For every admitted v : X -> Y:
- Same EntityOfConcern. X and Y designate the same exact EntityOfConcern. Similar labels, bridge claims, or one shared project do not establish this equality.
- No unsupported strengthening. Every claim in Y about that entity is recoverable as a consequence, conservative re-expression, or explicitly admitted aggregation of claims in the identified sources under the declared reference and representation semantics.
- Declared loss. Every omitted concern or claim family that affects receiving use is named, together with the condition under which the loss is admitted.
- Reference discipline. A changed effective reference scheme is explicit. If the change alters available operations or representation semantics, use A.6.3.RT; apply C.29 when the transition uses a declared mathematical lens. Do not call such a change formatting.
- No hidden retargeting. Subsystem-to-system, method-to-work, model-to-modeled-system, or episteme-to-publication changes are not same-EntityOfConcern viewing.
For a lightweight check, take each claim in Y—or each group covered by one rule—and point to the source claims and the selection, rewriting, or aggregation rule that licenses it. Mark omitted claim groups. If a result claim cannot be traced this way, treat it as a new claim rather than a viewing result. If support cannot be decided exactly, state the structural or domain check used as an approximation and what it cannot establish. Add a proof only when disagreement, risk, or the receiving use makes it necessary.
Truth of source claims is a separate evaluation. Conservativity says what Y is licensed to claim from the sources; it does not establish that those claims are true in the world or adequate for a decision.
A.6.3:4.4 - Keep optional viewpoint selection and view membership separate
For the current use of receiving episteme Y, name the describing use and exact viewpoint P only when that selection changes what the receiver reads or checks. Keep Y, its EntityOfConcern, the use, and P distinct. Selecting P is outside C.2.1 identity and does not make E.17.0 conformance obtain.
After Y is identified, apply E.17.0 only when the current use needs U.View membership:
EpistemeViewpointConformanceRelation(Y,P) obtains
-> the same episteme Y is a U.View
Directly authored Y can be a view without any A.6.3 source relation. Conversely, a valid A.6.3 construction can yield Y that fails P’s concern-coverage or semantic-form rules and therefore is not a view under P.
A.6.3:4.5 - Distinguish direct and correspondence-mediated construction
Direct viewing. Y is constructed from X and fixed configuration only. The declaration names the exact claim selection or rewriting rule and any loss. No generic correspondence object is required.
Correspondence-mediated viewing. Y depends on several exact source epistemes or on exact relations between their claim-bearing contents. Recover each direct correspondence, realization, trace, equivalence, or consistency relation under its governing pattern before using it. Then identify the C.2.1 episteme that states or describes those relations if the construction must cite it.
Plain correspondence model may name that exact claim-bearing episteme for convenience. It is not a public U.CorrespondenceModel kind, and its graph edges or table cells do not establish the direct relations. If a needed relation lacks a governor, return the exact missing-relation blocker or use A.6.RCD.
The viewing declaration cites the exact source epistemes and exact correspondence claims on which Y depends. If Y asserts facts about a correspondence episteme, evidence, or evaluation result, those assertions belong to Y’s claim content and follow C.2.1’s identity rule. The cited objects remain independently identified, and the assertions still require the support specified by the viewing law.
A.6.3:4.6 - Keep mathematical construction, work, production, and publication distinct
Describe querying, rewriting, modeling or rendering in ordinary practitioner terms. When the account claims a particular dated U.Work occurrence, establish its A.13 basis and A.15.1 admission; identify the system that performed the work and the method it used. The source epistemes, parameters, tools, and receiving entities participate only through their direct relations or A.6.1 operation bindings.
If that work first constitutes exact episteme Y and the identity-inception claim matters, A.15.PROD governs the local work/change/identity claim. Neither work nor inception establishes conservativity or E.17.0 conformance.
If Y is made available, E.24.PUB separately identifies the publication occurrence, publication form, and U.PresentationCarrier. Publication neither creates the A.6.3 construction nor grants U.View membership.
A.6.3:4.7 - Preserve composition and replay
The selected formal substrate supplies the identities, admitted compositions, and arrow equivalence. For fixed source epistemes, rules, reference semantics, correspondence dependencies, and configuration:
- identity viewing preserves the same C.2.1 episteme;
- composing
f : X -> Ywithg : Y -> Zgives the admitted compositecompose(g,f) : X -> Zunder A.6.2 P3; - if a separately declared construction operation is deterministic, replay with the same admitted inputs yields the same receiving C.2.1 identity discriminators;
- random seeds, model editions, external service state, or timing that can change Y are explicit inputs to the work or declaration, not hidden meta;
- a normalization repeat claim identifies
n_X : X -> Yand the next arrown_Y : Y -> Z, establishesZ = Yunder C.2.1, and witnessescompose(n_Y,n_X) ≃ n_Xunder the declared arrow equivalence. OneX -> Yarrow is self-composable only when X = Y.
A composition requires the exact middle episteme to match. A claim that two routes yield the same receiving episteme requires equality of all three C.2.1 identity discriminators; representation equivalence alone does not establish that identity. The repeat claim requires a fixture or proof under A.6.2 P4.
A.6.3:4.8 - Stop at the lightest sufficient statement
For ordinary use, this can be enough:
Safety summary Y is conservatively constructed from plant description X; both concern Plant-7; Y omits maintenance-cost claims and introduces no safety claim not recoverable from X.
Add a reusable declaration, explicit mathematical arrow, correspondence episteme, evaluation result, work occurrence, production claim, or publication objects only when a named receiving work or decision depends on that object.