#Typed Guard Macros for Kinds + USM (Annex)

C.3.A · Cluster C.I - Core CALs / LOGs / CHRs · Stable · Part C - Kernel Extension Specifications

#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.

One-line summary. These guard macros combine C.3 declaration compatibility, the exact C.3.2 candidate judgment when an actual candidate is current, RoleMask and KindBridge declarations/relations, and A.2.6 Scope without collapsing them. A claim quantified over a kind can be checked at declaration level; applying that claim or a capability to one candidate additionally requires J(candidate, kind, signatureEdition, slice). true, false, and unknown remain classification values, while allow/refuse remains a separate guard disposition. KindAT never appears in a guard.

Status. Normative for macro obligations, evaluation order, three-valued/fail-closed discipline, and the conformance checklist; informative for decision trees, examples, and implementation-like skeletons.

Placement. Part C (Kinds), identifier C.3.A. Audience: engineering managers, editors, reviewers, assurance leads, and authors of regulatory, evidence, ESG, and Method–Work checks.

Depends on.

• A.2.6 USM: exact U.ContextSlice, Claim/Work scope, Gamma_time, scope bridges, and SpanUnion.
• C.3/C.3.1: exact local kinds and obtaining U.SubkindOf relations.
• C.3.2: KindSignature declaration epistemes, J(candidate, kind, signatureEdition, slice), true/false/unknown, and optional extension representations.
• C.3.3: obtaining KindBridge relations and separate bridge-assertion epistemes carrying CL^k, loss, evidence, definedness, and admitted use.
• C.3.4: RoleMask and MaskAdapter declaration epistemes and J_mask(candidate, kind, kindSignatureEdition, roleMaskEdition, slice).
• C.3.5: KindAT as an editorial facet forbidden in guards.
• C.2.2/C.2.3 and Part B: F–G–R, formality on the owning episteme, bridge consequences, and scope congruence.
• A.15/A.15.1: the separation of capability, plan, exact actual Work occurrence, and every episteme about it.

Use this Annex when a receiving action must check one or more of these without blending them:

#Keywords

• declaration compatibility
• exact candidate judgment
• true/false/unknown
• guard refusal
• regulatory
• assurance
• ESG
• Method-Work.

#Relations

#Content

#Purpose and audience

Use this Annex when a receiving action must check one or more of these without blending them:

1. the declaration-level compatibility of a claim's quantified kind with a consumer's expected kind;
2. the classification of one exact candidate under one exact signature edition and slice;
3. Claim or Work scope coverage;
4. cross-context kind and scope bridges and their R consequences;
5. a RoleMask declaration and exact masked judgment; or
6. an actual capability use or Work occurrence whose input/output candidates are typed.

The practical gain is a readable refusal reason. “The kinds are incompatible”, “the candidate is known not to satisfy the criterion”, “classification is unknown”, “scope does not cover”, “a bridge is unavailable”, and “the guard refuses use” remain different outcomes.

#Problem

Older guard shorthand used one two-valued “membership defined” question for several different jobs. That erased the exact candidate and signature edition, collapsed unavailable support into known failure, made a refusal look like a classification result, and allowed a record or bridge assertion to manufacture target truth. Method–Work use added another collapse when a JobSlice, capability row, plan, or log was read as the performed Work occurrence.

C.3.A restores two levels:

• declaration level: which exact local kind and KindSignature edition a claim quantifies over, and whether that kind is compatible with the receiver's expected kind under same-context order or an obtaining KindBridge; and
• candidate-use level: whether one exact target-side candidate satisfies the receiver's exact declaration in that exact slice, with the claim-kind consequence supplied only by the already established same-context order or cross-context bridge.

#Shared outcome model

All guards obey these invariants.

1. Exact declarations. A kind designator never substitutes for the exact KindSignature edition needed by the use.
2. Candidate only when current. A universally quantified claim or proof can be checked for declaration compatibility without inventing a wildcard candidate. Actual application, test attachment, capability input/output use, or other candidate-bearing action pins the candidate and evaluates the four-input judgment.
3. Three classification values. true means the criterion is known to hold; false means it is known to fail; unknown means the evaluation cannot settle because evidence or a declared dependency is unavailable or the candidate is outside the evaluation domain.
4. Separate guard disposition. A guard returns an action disposition such as allow or refuse. Both false and unknown normally cause fail-closed refusal, but the guard MUST preserve which classification value it consumed.
5. Scope separation. Scope coverage is a USM predicate over a named slice. It does not classify the candidate or repair kind compatibility.
6. Bridge separation. An obtaining KindBridge relation connects exact source and target kinds. Its separate bridge assertion supplies mapping, CL^k, loss, evidence, definedness, and admitted use; neither object creates a target kind, signature, or judgment.
7. R-only consequences. Justified scope- and kind-bridge consequences affect R only. They do not change F, G, or classification truth.

#Normative guard macros

Names such as Guard_TypedClaim are editorial handles. A context may alias them only when the same objects, values, and refusal distinctions remain recoverable.

#Guard_TypedClaim — declaration-level admission

Intent. Decide whether claim C, quantified over local kind k_claim, may enter a receiving use restricted to kind k_receive in TargetSlice, without claiming anything yet about an unnamed candidate.

Guard_TypedClaim(C, k_claim, claimSignatureEdition, k_receive, receiveSignatureEdition, TargetSlice, thresholds?) SHALL:

1. recover the exact KindSignature declaration episteme editions whose respective EntityOfConcern values are k_claim and k_receive, and whose evaluation domains and effective reference schemes cover the declared use; when both roles use the same kind and edition, state that identity rather than duplicating the declaration;
2. establish declaration-level kind compatibility:
   • in one context, the kinds are identical or SubkindOfObtains(k_receive, k_claim; effectiveReferenceScheme) holds under C.3.1, with an identified R_sub : U.SubkindOf occurrence only when occurrence identity is needed; or
   • across contexts, an obtaining KindBridge relates exact source k_claim and target k_receive under the paired source and target KindSignature editions, and a separate current bridge assertion states the mapping, applicability, loss, CL^k, evidence, and admitted receiving use;
3. require U.ClaimScope(C) to cover the exact TargetSlice and require an explicit Gamma_time selector;
4. apply only the justified bridge consequences to R;
5. check evidence freshness separately when the admission implies reliance; and
6. check a policy-required formality threshold on the exact claim or declaration episteme that owns the value.

The same-context direction above is contravariant only for restricting a universally quantified claim: a claim over Vehicle may enter a PassengerCar-restricted use when PassengerCar is a subkind of Vehicle. It is not a generic compatibility direction for producer outputs, operation arguments, mutable positions, or arbitrary typed slots; each such use states its own variance rule. This guard MUST NOT invent an anonymous candidate or infer a candidate classification from declaration compatibility.

#Guard_CandidateUse — apply a typed claim to an exact candidate

Intent. Decide whether claim C, quantified over k_claim, may be used for exact target-side candidate candidate in a receiving use restricted to k_receive.

Guard_CandidateUse(C, candidate, k_claim, claimSignatureEdition, k_receive, receiveSignatureEdition, TargetSlice) SHALL:

1. identify the candidate under its direct governor before classification;
2. satisfy Guard_TypedClaim for the same claim-kind and receiving-kind editions and slice;
3. evaluate J(candidate, k_receive, receiveSignatureEdition, TargetSlice);
4. continue candidate-bearing use only on true: for a same-context proper subkind, the already established SubkindOfObtains(k_receive, k_claim; RS) supplies the monotone claim-kind consequence; for a cross-context use, rely only through the obtaining KindBridge and its current assertion, without inventing a source-context candidate judgment;
5. refuse on known false while retaining that value; and
6. refuse on unknown while retaining the missing dependency, unavailable support, or out-of-domain reason.

Evidence may support a classification assertion, but record presence, bridge presence, or guard invocation MUST NOT make the candidate satisfy the receiving criterion. When k_claim and k_receive are identical under one declaration edition, record that identity and evaluate the candidate once.

#Guard_TypedJoin — compose typed producers and consumers

Intent. Compose producer A, which declares output kind k_A, with consumer B, which expects input kind k_B.

Guard_TypedJoin(A, k_A, edition_A; B, k_B, edition_B; TargetSlice) SHALL:

1. pin both declaration episteme editions;
2. establish output-to-input compatibility in the covariant flow direction:
   • in one context, the kinds are identical or SubkindOfObtains(k_A, k_B; effectiveReferenceScheme) holds; or
   • across contexts, an obtaining KindBridge maps k_A to exact target-side kind k_A', its separate assertion carries the current mapping and loss basis, and k_A' is identical to k_B or SubkindOfObtains(k_A', k_B; targetReferenceScheme) holds;
3. compute serial scope as the intersection of the two governed scopes and require coverage of TargetSlice;
4. route bridge consequences to R and check freshness separately; and
5. when an actual produced candidate enters B, evaluate J(candidate, k_B, edition_B, TargetSlice) and continue only on true, preserving false and unknown separately from refusal.

Declaration compatibility alone MUST NOT classify a future or actual output. Scope widening MUST NOT repair a type mismatch. The universal-claim variance rule in Guard_TypedClaim does not reverse this producer-to-consumer direction.

#Guard_MaskedUse — exact RoleMask use

Intent. Use exact candidate candidate under a named RoleMask declaration in TargetSlice.

Guard_MaskedUse(artifact, candidate, kind, kindSignatureEdition, roleMaskEdition, TargetSlice) SHALL:

1. recover the exact C.2.1 RoleMask declaration episteme, its base kind, pinned base signature edition, intended use, candidate-feature constraints, bindings, dependencies, and definedness;
2. check artifact scope separately through USM;
3. evaluate J_mask(candidate, kind, kindSignatureEdition, roleMaskEdition, TargetSlice);
4. continue only on true, refuse while preserving known false, and fail closed while preserving unknown;
5. keep context predicates out of the candidate-feature criterion; and
6. for cross-context use, establish the KindBridge relation and assertion, target declarations, and any separate MaskAdapter declaration episteme before evaluating the target masked judgment.

A mask name is not a kind synonym. Repeated mask use can trigger review for a separately identified local kind and independently obtaining U.SubkindOf relation; no guard or catalog action performs that admission.

#GuardSpanUnionTyped — parallel support lines

Intent. Publish SpanUnion for the same typed claim supported by independent lines.

For each line, the guard SHALL:

1. recover the same governed claim, quantified kind, and signature edition;
2. satisfy declaration-level typed admission in that line's slice;
3. when a line's evidence is candidate-specific, bind each exact candidate and its exact judgment rather than treating a row label as classification;
4. preserve line-specific bridge consequences and freshness;
5. provide the USM independence justification; and
6. include no slice outside the union of covered line scopes.

If lines quantify over genuinely different kinds, normalize through separately justified kind relations or publish distinct claims; do not hide the difference in SpanUnion.

#GuardXContextTyped — cross-context typed reuse

Intent. Reuse claim C from a source context in target TargetSlice while keeping scope translation, kind correspondence, and target classification separate.

Guard_XContext_Typed(C, sourceKind, sourceSignatureEdition, targetKind, targetSignatureEdition, TargetSlice, candidate?) SHALL:

1. recover an obtaining Scope Bridge and its applicable congruence assessment when Claim scope crosses context;
2. recover an obtaining KindBridge relation with exact source/target kind participants and its separate bridge assertion with pinned scheme/signature editions, mapping rule, definedness, CL^k, loss, evidence, and admitted use;
3. recover the independently authored target KindSignature edition;
4. require translated Claim scope to cover TargetSlice;
5. when an actual candidate is current, evaluate the fresh target judgment J(candidate, targetKind, targetSignatureEdition, TargetSlice) and preserve all three values;
6. apply the justified scope- and kind-bridge consequences to R only; and
7. make the separate allow/refuse decision.

A source judgment may support reliance but MUST NOT be copied as target truth. If no candidate is current, the guard ends at declaration-level compatibility and scope; it does not fabricate one.

#Evaluation semantics and order (normative)

E-01 (Order). Recover exact declarations and kind compatibility first; check Scope coverage second; evaluate an exact candidate only when the receiving action is candidate-bearing; then apply R consequences, freshness, and policy thresholds before the separate action disposition.

E-02 (Determinism). With fixed candidates when any, kind/signature editions, slices, bridge/assertion editions, dependencies, and time selectors, the judgments and guard predicates MUST be reproducible. Implicit “latest” is forbidden.

E-03 (Three values). Every current C.3.2 or C.3.4 classification consumed by a guard MUST retain true, false, or unknown. Missing evidence, unavailable declared dependency, or out-of-domain input MUST NOT be coerced to false.

E-04 (Fail-closed without truth rewrite). A required false, unknown, missing declaration, non-obtaining relation, unavailable bridge assertion, or uncovered Scope causes refusal. The refusal is not itself a classification value or an assertion that the relevant world-side relation fails to obtain.

E-05 (Weakest link and bridge consequence). Chained bridge assessments use the governed weakest-link rule. The receiving R path records each relied-on bridge/assertion; neither F nor G nor a judgment value is modified.

E-06 (Predicate separation). Declaration compatibility, candidate classification, Scope coverage, evidence freshness, bridge applicability, capability fit, and action disposition SHALL remain separately inspectable predicates.

#Conformance checklist (normative)

#Proven-equivalent aliases

A context-specific guard alias is equivalent only when all required objects, inputs, classification values, bridge distinctions, and disposition boundaries can be recovered. Similar wording or the same final allow/refuse bit is insufficient.

#Bridge consequences

Phi(CL_scope) and Psi(CL_kind) are monotone non-increasing consequences on the receiving R path under the governing bridge patterns. This Annex prescribes no numeric form. It never performs arithmetic on F or G.

#Decision trees (informative)

D1 — Admit a quantified claim.

1. Pin the quantified claim kind, receiving kind, and both exact signature editions.
2. In one context, require the receiving kind to be identical to or a subkind of the claim kind; across contexts, recover the exact source-claim to target-receiving KindBridge relation and assertion.
3. Check Claim scope against the exact TargetSlice and Gamma_time.
4. Apply R consequences and freshness/threshold checks.
5. Return the separate action disposition. Do not ask for a candidate unless the receiving use applies the claim to one.

D2 — Apply the claim to a candidate.

1. Identify the candidate under its direct governor.
2. Complete D1.
3. Evaluate the exact four-input target judgment under the receiving-kind declaration; use the already established order or bridge for the claim-kind consequence.
4. On true, continue; on false, refuse as known failure; on unknown, refuse and retain the non-settlement reason.

D3 — Compose or cross a context.

1. Pin source and target declarations.
2. Recover the obtaining kind relation/bridge and separate assertion; recover Scope Bridge separately.
3. Check the serial or translated scope.
4. If an actual output/candidate is current, evaluate it under the target declaration.
5. Apply R consequences and decide separately.

D4 — Publish a union.

1. Complete the relevant D1/D2 checks per line.
2. Demonstrate support-line independence.
3. Publish only the supported union; retain line-specific classifications and bridge consequences.

#Guard anti-patterns and remedies (informative)

#Worked examples (informative)

E1 — Same-context braking claim. A policy quantified over Vehicle pins VehicleSignature@v4; the receiver pins PassengerCarSignature@v3. Declaration admission establishes SubkindOfObtains(PassengerCar, Vehicle; plantVehicleScheme). Applying the policy to VIN-17 evaluates J(VIN-17, PassengerCar, v3, S-plant); on true, C.3.1 monotonicity supplies the Vehicle-side consequence needed by the universal claim. A missing axle dependency yields unknown and a separate refusal.

E2 — Cross-plant reuse. An obtaining KindBridge relates source Vehicle to target TransportUnit; its assertion records a collapsed EV/ICE distinction and CL^k=2. The target signature is independently authored. Plant-B evaluates its exact vehicle candidate under that target edition; the source result is only support, and bridge consequences lower R.

E3 — API adapter. A producer declares Request; a consumer expects AuthenticatedRequest. Declaration compatibility fails until an adapter and target declaration are recovered. For request req-884, unavailable key-validation support yields target unknown; the consumer refuses without asserting that the request is known unauthenticated.

E4 — Masked clinic use. The guard designates the exact AdultPatient@Clinic RoleMask declaration, base signature edition, patient candidate, and slice. Unavailable date-of-birth support yields unknown; the mask label and EHR row do not classify the patient.

#Rationale

One final allow/refuse bit is operationally convenient but ontologically poor. Keeping declarations, candidate judgments, Scope, bridges, evidence, and disposition separate lets a reviewer see which repair is needed and prevents a guard from becoming a hidden relation, assertion, or evidence-to-truth converter.

#C.3.A:Annex A - Regulatory and compliance alignment [A/I]

#C.3.A:A.1 Purpose and fit

Regulations name categories such as Adult person, Class II medical device, Personal data, and Lease. A local context needs both a faithful category correspondence and explicit jurisdiction/version/time applicability. The kind channel answers “about what”; USM Scope answers “where and when”; neither answers whether one exact local candidate satisfies the target criterion.

#C.3.A:A.2 Normative obligations

C-REG-1 (Regulatory declarations). Each used regulatory category SHALL be an exact authority-context local kind with a separately identified KindSignature declaration episteme edition. Any F value characterizes that episteme, not the kind.

C-REG-2 (Kind correspondence). Cross-context category use SHALL recover an obtaining KindBridge relation between exact authority and local kinds plus a separate bridge assertion with mapping, pinned editions, preservation/loss, CL^k, evidence, definedness, and admitted use.

C-REG-3 (Scope). Jurisdiction, effective dates, grace periods, and other genuinely contextual applicability conditions SHALL be Claim scope over exact context slices with explicit Gamma_time. A product-family or platform distinction belongs in Scope only when it is genuinely a context-slice dimension of the claim; when it classifies the target entity, recover it as an exact kind and, for candidate-bearing use, an exact candidate judgment. A direct candidate feature remains with its own governor and SHALL NOT be smuggled into Scope.

C-REG-4 (No synonym shortcut). A legal label, translation row, or policy card SHALL NOT substitute for the KindBridge relation, its assertion, or the target declaration.

C-REG-5 (Exact candidate use). Whenever a policy is applied to candidate candidate, the guard SHALL evaluate J(candidate, localKind, localSignatureEdition, localSlice) and retain true, false, or unknown. Declaration compatibility alone is insufficient.

C-REG-6 (Consequences). Justified kind- and scope-bridge consequences SHALL affect R only. They SHALL NOT alter F, G, or the candidate judgment.

C-REG-7 (Editioning). A change in law that changes the criterion creates another signature episteme edition; a change in applicability changes Scope. C.3.1 decides kind continuity. Guards SHALL pin editions and time and SHALL NOT rely on “latest”.

C-REG-8 (Local adaptation). A local nuance MAY use a RoleMask declaration. If it becomes a stable conceptual distinction, the context SHALL separately identify any new local kind and establish its obtaining subkind relation; mask reuse does not perform that change.

#C.3.A:A.3 Regulatory guards

Guard_RegAdopt(P, candidate, authorityKind, authoritySignatureEdition, localKind, localSignatureEdition, S_local).

1. Check P's governed scope and explicit time against S_local.
2. Recover the exact authority/local declarations, KindBridge relation, and bridge assertion.
3. Check bridge applicability and route its consequence to R.
4. Evaluate J(candidate, localKind, localSignatureEdition, S_local).
5. Continue only on true; retain known false or unknown before refusing.
6. Check freshness of relied-on regulatory and candidate support separately.

Guard_RegChange(change, impactedDeclarations, impactedScopes).

1. Decide whether the change alters criterion, reference scheme, applicability, or more than one.
2. Author the required signature episteme edition and let C.3.1 settle kind continuity.
3. Update Scope independently when jurisdiction/version/time coverage changes.
4. Reassess the bridge assertion's mapping, loss, CL^k, evidence, and admitted use.
5. Evaluate affected exact candidates for the new receiving use under the new declaration edition while preserving every prior judgment indexed to its prior edition and slice; do not edit a set representation or rewrite historical judgments as a substitute.

Guard_RegXContextUse(P, candidate, sourceKind, targetKind, targetSignatureEdition, S_target). Apply Guard_XContext_Typed and then the exact target candidate judgment. A missing target dependency yields unknown; it is not cured by a high bridge assessment.

#C.3.A:A.4 Worked examples [I]

Adult dosage across jurisdictions. Authority kind AdultPerson@RegY uses threshold 18; hospital kind AdultPatient uses 21. The obtaining KindBridge and its assertion state the boundary loss and CL^k=1. For patient P-44, the hospital evaluates its target signature edition in the dated formulary slice. Missing DOB support gives unknown; the guard refuses without asserting that P-44 is a non-adult.

GDPR and CCPA. Two source kinds relate to independently identified product-context kinds through separate bridges/assertions. Each policy has its own jurisdiction/time Scope. A data item is governed by a fresh target judgment; an alias table is support, not classification.

Export control. The shipping policy pins the target product signature edition, shipment candidate, destination/end-use slice, and date. Category correspondence and Scope translation have separate bridges. The exact product judgment and the shipping guard disposition remain separate; higher residual risk may require manual review.

IFRS and US GAAP Lease. Each authority kind and local corporate kind remains independently identified. The bridge assertion records the short-term-exception loss. Test planning targets boundary candidates under pinned target declarations rather than treating one shared label as truth.

#C.3.A:A.5 Guidance and migration [I]

1. Inventory regulatory claims, exact category declarations, and applicability slices.
2. Recover or author target KindSignature declaration editions; keep F on those epistemes.
3. Establish KindBridge relations and separate assertions with loss and admitted use.
4. Rewrite candidate-bearing guards to pin candidate, local kind, signature edition, and slice.
5. Preserve unknown and record refusal separately.
6. Route Scope through USM and bridge consequences through R.
7. Use RoleMask declarations for local procedural tailoring; separately establish a new kind/order relation only when the distinction truly becomes conceptual and stable.

#C.3.A:A.6 Manager's compact pattern [I]

• Where and when? Claim scope over exact context slices.
• About what? Exact local kind and signature declaration; KindBridge relation/assertion if foreign.
• Which exact thing? Fresh target J(candidate, kind, signatureEdition, slice).
• Can we act? A separate guard disposition after scope, judgment, bridge, freshness, and policy checks.

#C.3.A:Annex B - Assurance lanes and evidence design [A/I]

#C.3.A:B.1 What typed assurance adds [I]

VA can prove a claim quantified over an exact declared kind; LA can exercise exact candidates and boundary cases under pinned editions and slices; TA can qualify the tools used to produce support. None of those lanes turns evidence existence into classification truth.

#C.3.A:B.2 Normative obligations

EA-1 (Declaration and candidate binding). Every VA/LA artifact SHALL cite the governed claim, exact quantified kind and signature edition, and assumed Scope. Candidate-specific evidence SHALL additionally name each exact candidate and its four-input judgment.

EA-2 (Subkind coverage). A claim over kind k SHALL justify coverage over relevant obtaining subkind relations and paired signature editions. RoleMask rows may cover named procedural uses but SHALL NOT silently stand in for a stable subkind.

EA-3 (Three values in evidence use). A test, observation, or proof may support a classification assertion. An unavailable evidence dependency yields unknown; failed evidence retrieval MUST NOT be recorded as candidate false.

EA-4 (Independent unions). SpanUnion SHALL include a support-line independence account and preserve per-line candidate judgments and bridge consequences.

EA-5 (Bridges). Cross-context evidence use SHALL recover Scope Bridge separately from KindBridge relation/assertion, use the independently authored target declaration, and evaluate target candidates afresh. Consequences affect R only.

EA-6 (Freshness). Evidence windows and tool/declaration editions SHALL be explicit and tied to the governed slice. Expiry causes refusal or unknown at the predicate it disables; it does not widen Scope.

EA-7 (TA separation). Tool qualification SHALL remain distinct from content proof, candidate facts, classification judgment, and receiving disposition.

EA-8 (No scope-by-wording). More general wording, more matching candidates, or additional evidence-matrix rows SHALL NOT widen G. A ΔG+ change requires the new support or sufficiently congruent bridge basis required by A.2.6; otherwise retain or narrow the declared Scope.

#C.3.A:B.3 Evidence matrix [I]

Rows plan declared distinctions; they do not classify every candidate. A proof-only row may remain declaration-level when it genuinely proves a universal claim. A test or monitoring row becomes candidate-bearing and records exact judgments for the exercised candidates.

#C.3.A:B.4 VA lane [A/I]

• VA-1. A proof carrier SHALL cite the exact claim, quantified kind, KindSignature edition, and assumed scope slices.
• VA-2. A proof of a universal claim need not invent a candidate; application to an actual candidate uses Guard_CandidateUse separately.
• VA-3. Cross-context proof reliance SHALL recover both bridge channels, the target declaration, loss, and R consequences.
• VA-4. Tool-kernel qualification belongs to TA and does not raise the declaration's F or candidate truth.

Example: a proof over PassengerCarSignature@v4 assumes a dry-road slice. Reuse at Plant-B requires bridge/scope settlement. Application to VIN-17 then uses the Plant-B target signature and exact target judgment.

#C.3.A:B.5 LA lane [A/I]

• LA-1. Each test or monitoring campaign SHALL state row declaration editions, slice columns, exact tested candidates, and their judgments.
• LA-2. Boundary probing SHALL distinguish criterion boundaries from Scope boundaries.
• LA-3. A KindBridge assertion that records collapsed distinctions SHALL lead to explicit coverage repair; it does not alter target truth.
• LA-4. Freshness and SpanUnion independence SHALL remain explicit.

Example: rows PassengerCar and LightTruck use pinned signature editions; columns cover dry/wet slices. The tested VINs are exact candidates. A missing sensor dependency for one VIN yields unknown, not a negative vehicle classification.

#C.3.A:B.6 TA lane [A/I]

Qualify provers, checkers, measurement pipelines, and classifiers separately. A classifier output can support an assertion about J; the tool neither becomes the candidate nor makes the governed criterion hold. Version drift may make the support unavailable and hence produce unknown for a candidate-bearing use.

• TA-1. Every tool whose qualification is relied on by VA or LA SHALL identify its exact version and qualification status, and the receiving guard SHALL recover that declaration when the reliance is current.
• TA-2. Missing or weaker tool qualification MUST NOT be hidden by lowering the owning episteme's F or widening G. The receiving policy may require additional independent support, reduce or condition R, or refuse the use while preserving the exact unavailable-support reason.

#C.3.A:B.7 Evidence guards

Guard_EvidencePlan_Typed SHALL check exact row declaration editions, exact slice columns, bridge/assertion needs, candidate-selection policy, freshness, independence, and TA declarations. Planning rows do not count as candidate judgments.

Guard_EvidenceAttach_Typed SHALL bind every evidence unit to its exact claim/use, row declaration, slice, exact candidate when current, judgment value, support relation, freshness, and bridge consequences. It SHALL preserve unknown and the separate attach/refuse disposition.

#C.3.A:B.8 Anti-patterns and remedies

#C.3.A:B.9 End-to-end example [I]

A two-plant braking claim pins the PassengerCar declaration and Plant-A scope. VA proves the quantified claim over that declaration. LA tests exact VINs in dry/wet slices and records their judgments. TA identifies tool versions. Plant-B reuse recovers both bridges, the target declaration, loss and R consequences; each Plant-B candidate is evaluated afresh before evidence is attached.

#C.3.A:Annex C - ESG and Method–Work guards

#C.3.A:C.1 ESG obligations (normative)

When a state transition publishes or relies on a claim quantified over kinds, the ESG guard SHALL:

1. pin the claim, exact quantified claim kind, receiving kind, and both needed KindSignature editions;
2. establish the correct same-context restriction direction or the exact source-claim to target-receiving KindBridge relation and separate assertion;
3. check Claim scope and explicit Gamma_time;
4. when one or more actual candidates are part of the transition, evaluate each exact four-input target receiving-kind judgment and preserve all three values;
5. when a RoleMask is used, recover its declaration edition and evaluate the exact masked judgment;
6. apply justified bridge consequences to R only;
7. check formality and freshness on their actual owners; and
8. return a separate state-transition disposition.

ESG MUST NOT widen G to hide incompatibility, treat a label as a candidate judgment, or convert unknown to false.

#C.3.A:C.2 Method–Work obligations (normative)

This Method–Work slice is conditional; it is not a definition that makes every actual change agentic, capability-held, planned, method-mediated, or Work. Open its capability/method/WorkPlan entry checks only when those objects and an A.15.1 Work use are current. A natural, spontaneous, formal, jointly caused, or non-separable U.Transformation remains under A.3/A.3.4 and does not acquire a fictive performer, role assignment, method, capability, plan, or Work to satisfy this guard. A broader scale-free-agency or Work decision remains with A.13 and A.15.1; planned C.9 may later consolidate an agency-characteristic profile but supplies no current governing force. This annex neither settles nor forbids that decision. Reflexive cases require separately grounded acting and affected positions, while joint or non-separable cases keep their direct dynamics, interaction, or causality governors rather than forcing one arbitrary actor-target split.

When the Method–Work use is current, it has two different boundaries.

Prospective entry. Before execution, a guard may decide that a holder capability, method, intended U.WorkPlan, JobSlice, and candidate inputs are sufficient to start. That decision SHALL NOT claim that Work already occurred. The capability instance, capability statements or currentness assessments, fit predicates, WorkPlan, JobSlice, and entry record remain distinct.

Actual result or acceptance. When performed Work is current, the guard SHALL identify exact W : U.Work as an independently grounded, world-side, dated 4D Work occurrence under A.15.1. W is not the U.Work kind, JobSlice, capability, plan item, log, card, row, or assertion. Any plan, log, result record, or assurance record about W is a separate episteme that designates W.

A conforming Method–Work check SHALL:

1. require the capability's governed Work scope to cover exact JobSlice with explicit time;
2. check capability measures, qualification/currentness, and fit as separately governed predicates;
3. pin every expected input/output local kind and signature edition;
4. for every actual input candidate, evaluate J(inputCandidate, expectedInputKind, inputSignatureEdition, JobSlice) and preserve all three values;
5. use exact RoleMask declarations and masked judgments when procedural tailoring is current;
6. establish exact target bridges/declarations and fresh target judgments for cross-context candidates;
7. before execution, return only an entry disposition and keep W absent;
8. after execution, identify W independently and, for every actual output candidate relied on, evaluate the exact output judgment;
9. keep W, inputs, outputs, JobSlice, capability, plan, logs, and assertions distinct; and
10. refuse fail-closed on false or unknown without rewriting either value.

#C.3.A:C.3 Ready-to-use skeletons

ESG_TypedGate(Claim, claimKind, claimSignatureEdition, receiveKind, receiveSignatureEdition, TargetSlice, candidates?). Apply Guard_TypedClaim to the exact claim and receiving kinds; for each actual candidate apply Guard_CandidateUse with both declaration editions; apply bridge, freshness, and policy predicates; return the separate transition disposition.

MethodWork_EntryGate(Capability, WorkPlanRef, JobSlice, inputCandidates, inputDeclarations). Check Work scope, capability/qualification/fit predicates, exact input judgments, masks, bridges, and freshness. Return “entry allowed/refused”. Do not create or identify W.

MethodWork_ResultGate(W, JobSlice, actualInputs, actualOutputs, declarations, ResultRecordRef?). First recover the independently grounded dated W under A.15.1. Then evaluate exact input/output candidate judgments, check scope and any acceptance predicates, and keep any ResultRecordRef as a separate episteme designating W.

#C.3.A:C.4 Worked examples [I]

ESG braking policy. The claim pins VehicleSignature@v4 and the dry/wet TargetSlice. The consumer is restricted to PassengerCar, and SubkindOfObtains(PassengerCar, Vehicle; plantVehicleScheme) holds under the paired exact declaration editions. For VIN-17, evaluate J(VIN-17, PassengerCar, passengerCarEdition, TargetSlice)=true; C.3.1 monotonicity then supplies the Vehicle-side classification needed by the universal claim. An unavailable brake-configuration dependency would yield unknown, and the transition would refuse separately.

Risk-score Work entry and occurrence. ComputeRiskScore capability is considered for request req-884 in JobSlice api-v2.3/eu-west/t-204. The entry guard evaluates the request under the pinned AuthenticatedRequest signature. If true, it may admit execution; no Work occurrence yet follows. After execution, actual W = RiskScoreRun-2026-07-22T10:03Z-884 : U.Work is independently grounded as the dated world-side occurrence. RiskScoreRunLog-884 is a separate episteme designating W. The output score value is a separate candidate evaluated under its declared output kind and signature edition.

Cross-context plant use. The source claim and source kind cross via separate Scope and KindBridge channels. Plant-B recovers its own target declaration and evaluates exact TransportUnit candidate TU-9. Bridge assertions affect R; they do not classify TU-9 or create the later Work occurrence.

#C.3.A:C.5 Anti-patterns and remedies

#C.3.A:End

---

Last Updated: 2026-08-05 — upstream FPF commit 3dbce514 (github.com/ailev/FPF)