#Typed Guard Macros for Kinds + USM (Annex)

Pattern C.3.A · Stable Part C - Kernel Extension Specifications

One‑line summary. Provides normative guard macros that combine USM Scope (A.2.6) with Kind‑CAL (C.3.x) so authors can gate state changes and compositions that quantify over kinds without conflating describedEntity (Kinds) with applicability (Scope G) or assurance (R). Includes decision trees, anti‑patterns, and examples (informative). AT (KindAT) is never used in guards.

Status. Mixed: — Normative: guard macro clauses, evaluation order, fail‑closed discipline, conformance checklist. — Informative: … decision trees, anti‑patterns, worked examples, macro skeletons.

Placement. Part C (Kinds), identifier C.3.A (Annex). Audience: engineering managers, editors, reviewers, assurance leads.

Depends on. — A.2.6 USM: U.ContextSlice, U.ClaimScope (G), U.WorkScope, ∈/∩/SpanUnion/translate, Γ_time policy, Bridge + CL (scope). — C.3.1: U.Kind, U.SubkindOf (⊑); C.3.2: KindSignature (with F) and Extension/MemberOf; C.3.3: KindBridge + CL^k (kind‑congruence) & loss notes; C.3.4: RoleMask. — C.3.5: KindAT (facet) — explicitly forbidden in guards. — C.2.2 F–G–R: weakest‑link, penalties to R only; C.2.3 F: F0…F9 (expression rigor). — Part B Bridges & CL: scope bridge semantics and CL ladder.

Purpose. Give Contexts a single set of guard shapes to: (a) admit typed claims safely, (b) compose typed claims/specs, (c) use RoleMasks properly, and (d) reuse across Contexts via both scope and kind bridges—without inventing new scales or conflating G, F, and R.

#Keywords

• Typed guard
• ESG
• Method-Work
• USM
• Kind-CAL
• regulatory profile.

#Relations

#Content

#Purpose & Audience

Purpose. Give Contexts a single set of guard shapes to: (a) admit typed claims safely, (b) compose typed claims/specs, (c) use RoleMasks properly, and (d) reuse across Contexts via both scope and kind bridges—without inventing new scales or conflating G, F, and R.

Audience. Engineering managers and reviewers who must read/author guards that are legible, deterministic, and auditable in context.

#Context & Problem

Projects often:

• treat “more abstract wording” as wider G,
• glue claims with incompatible describedEntity (kinds),
• move typed content across Contexts without declared bridges,
• or bake AT (abstraction vibe) into decision logic.

C.3.A fixes this by supplying guard macros that: — separate typed compatibility (kinds) from Scope coverage (USM), — require both bridges where needed, — push congruence penalties to R only, and — forbid AT in guards.

#Solution Overview (what these guards do)

All guards in this Annex share three invariants:

1. Fail‑closed. If any required predicate is undefined/false, the guard denies the transition.
2. Deterministic. Given a fixed TargetSlice (with explicit Γ_time) and published declarations, evaluation yields one outcome.
3. Separation of concerns. Typed compatibility (same‑Context ⊑ or KindBridge) is not Scope. Scope coverage is a USM set‑membership judgment over Context slices. Assurance penalties (Φ(CL) for scope bridges; Ψ(CL^k) for kind bridges) reduce R only.

#Normative Guard Macros

Notation. “SHALL” clauses are normative obligations. “Notes” are informative reminders. Names like Guard_TypedClaim are editorial handles; Contexts may alias them, but MUST preserve semantics. Macro names (e.g., Guard_TypedClaim) are editorial handles; Contexts may alias them provided the logical obligations are preserved.

#Guard_TypedClaim — admit a claim quantified over a kind

Intent. Approve a state transition that asserts Claim C which quantifies over U.Kind k at TargetSlice.

Guard_TypedClaim(C, k, TargetSlice, thresholds?) — SHALL include, in this order:

1. ScopeCoverage. U.ClaimScope(C) covers TargetSlice. (USM A.2.6)
2. Γ_time declared. TargetSlice SHALL specify Γ_time (point/window/policy). No “latest”. (A.2.6)
3. Kind definedness. MemberOf(?, k, TargetSlice) is defined and deterministic. (C.3.2 K‑05/K‑07)
4. Typed compatibility. 4.1 same Context: if C expects k′, require k ⊑ k′. (C.3.1) 4.2 Cross Context: if Contexts differ, require a declared KindBridge that maps k → k′ and publishes CL^k ≥ c with loss notes. (C.3.3)
5. Assurance penalties (R only). If step 4.2 used a KindBridge, the guard SHALL apply a monotone penalty Ψ(CL^k) to R. If a Scope bridge was used to move C’s Scope (USM), apply Φ(CL) to R. (C.2.2 + C.3.3 + Part B)
6. Evidence freshness (if trust is implied). Freshness windows and expiry checks SHALL be separate predicates (not Scope). (C.2.2)
7. Formality threshold (if ESG mandates). If the Context gates rigor, require U.Formality(C) ≥ F_k. (C.2.3)

Prohibitions. — AT forbidden. KindAT MUST NOT appear in this guard. (C.3.5 AT‑01/02) — No “domain” placeholders. Guards SHALL name an addressable TargetSlice, not a fuzzy “domain”.

#Guard_TypedJoin — compose two typed claims/specs (A → B)

Intent. Permit composition where A produces facts over k_A and B consumes k_B.

Guard_TypedJoin(A, k_A; B, k_B; TargetSlice) — SHALL include:

1. TypedCompat. 1.1 same Context: require k_A ⊑ k_B. 1.2 Cross Context: require KindBridge mapping k_A → k′_B with CL^k ≥ c and k′_B ⊑ k_B.
2. ScopeSerial. Compute Scope_serial = ClaimScope(A) ∩ ClaimScope(B). Require Scope_serial covers TargetSlice. (A.2.6)
3. Penalties (R only). Apply Ψ(CL^k) if a KindBridge was used; apply Φ(CL) if a Scope bridge was used. (C.2.2 / Part B / C.3.3)
4. Freshness. Guard SHALL assert required freshness windows for evidence along the serial path.
5. No type‑by‑scope. The guard MUST NOT widen Scope to “fix” a type mismatch; remedies are subkind introduction, adapter, or bridge.

Mask awareness. If B expects a RoleMask(k_B): either show A’s outputs already satisfy mask constraints, or add a documented mask adapter (see 4.3) and treat any contextual constraints as part of ScopeSerial.

#Guard_MaskedUse — use a RoleMask with a kind

Intent. Use U.Kind k under a RoleMask m in Context R.

Guard_MaskedUse(k, m, TargetSlice) — SHALL include:

1. MaskRegistered. RoleMask(k, m, version) is registered and versioned. (C.3.4 RM‑06)
2. MaskDeterminism. All mask constraints are observable on TargetSlice; if the mask narrows membership, it SHALL be deterministic. (RM‑03)
3. MaskType clarity. Mask SHALL declare its type: constraint / vocabulary / composite. (RM‑04)
4. Promotion cue. If mask is reused widely as a de‑facto subkind, editors SHOULD promote it to an explicit ⊑ link. (RM‑05)
5. Cross‑context use. If TargetSlice.Context ≠ owner(k).Context, require: 5.1 KindBridge with CL^k ≥ c; 5.2 MaskAdapter (if constraints need translation), deterministic; 5.3 Penalty Ψ(CL^k) to R. (RM‑07 + C.3.3)
6. ScopeCoverage. U.ClaimScope(artifact) covers TargetSlice. (A.2.6)

Prohibitions. — Mask ≠ Kind. Guards MUST NOT treat the mask name as a synonym for the Kind. (RM‑06)

#Guard\SpanUnion\Typed — publish parallel coverage across independent support lines

Intent. Publish SpanUnion of scopes for the same typed claim supported by independent lines L₁…Lₙ.

Guard_SpanUnion_Typed(C, k, {Lᵢ}) — SHALL include:

1. Per‑line discipline. For each line Lᵢ, first satisfy Guard_TypedClaim(C, k, Sliceᵢ) (or its Cross‑context variant) at the relevant slices/supports.
2. Independence justification. Publisher SHALL include a partition or certificate showing that essential components of Lᵢ are disjoint from Lⱼ (no shared weakest link). (A.2.6 §7.3)
3. Published scope. Scope_published = SpanUnion({Sᵢ}), where each Sᵢ is the serial scope for line Lᵢ.
4. No overreach. The union MUST NOT include slices not covered by any Sᵢ.
5. Typed consistency. The describedEntity (kind k) is the same across lines; if not, normalize via subkinds or adapters before union.

Note. Independence and union rules are USM‑native; this macro ties them to typed claims without adding new algebra.

#Guard\XContext\Typed — Cross‑context typed reuse (both bridges)

Intent. Reuse C quantified over k in another Context’s TargetSlice.

Guard_XContext_Typed(C, k, TargetSlice) — SHALL include:

1. Scope bridge. There exists a Scope Bridge b_s (source = owner(C).Context, target = TargetSlice.Context) with CL ≥ c_s. (Part B)
2. Kind bridge. There exists a KindBridge b_k (source = owner(k).Context, target = TargetSlice.Context) with CL^k ≥ c_k. (C.3.3)
3. Mapped scope coverage. Scope′ = translate(b_s, ClaimScope(C)) and Scope′ covers TargetSlice.
4. Mapped kind definedness. k′ = translate(b_k, k) and MemberOf(?, k′, TargetSlice) is defined.
5. Penalties (R only). Apply Φ(CL(b_s)) and Ψ(CL^k(b_k)) to R.
6. Loss notes. Publisher SHALL attach loss notes from both bridges (rig bias, collapsed subkinds, etc.).

Prohibitions. — Do not “merge” bridges; Scope and Kind are orthogonal channels. — Do not alter F or G due to CL/CL^k; penalties land in R only.

#Evaluation Semantics & Order (normative)

E‑01 (Order of checks). Guards SHALL check typed compatibility first (same‑Context ⊑ or KindBridge), then Scope coverage (USM), then apply penalties to R and verify freshness.

E‑02 (Determinism). Given fixed inputs (slices, bridges, versions), evaluation MUST be deterministic. “Latest” time, unversioned Standards, or implicit mappings are disallowed.

E‑03 (Fail‑closed). Undefined membership (MemberOf) or missing bridge MUST cause guard failure.

E‑04 (No AT in guards). AT is an editorial facet and MUST NOT be referenced. (C.3.5 AT‑01/02)

E‑05 (Weakest link on congruence). For chained bridges, effective CL / CL^k is the minimum of links.

E‑06 (Separation of predicates). Scope coverage and evidence freshness SHALL be distinct predicates; do not fold freshness into Scope or kinds.

Evaluation order. Apply checks in the order defined in §5 (E‑01): typed compatibility → Scope coverage → penalties to R → freshness.

#Conformance Checklist (normative)

#What counts as “proven‑equivalent” (editorial rule)

A Context may adopt a different surface phrasing iff the Context’s guard contains all obligations listed in the relevant macro, in the same logical roles (typed compatibility, Scope coverage, R penalties, freshness).

#Where penalties land (assurance calculus hook)

Norm. Φ(CL) (scope congruence) and Ψ(CL^k) (kind congruence) are monotone non‑increasing functions into R. Contexts SHALL calibrate them per policy; this Annex does not prescribe numeric forms.

#Minimal conceptual formulas (informative)

• R after bridges: R_final = R_base × Φ(CL_scope) × Ψ(CL_kind) (concept only).
• No arithmetic on F/G. F is ordinal (thresholds only); G is set‑valued (membership only).

#Decision Trees (informative)

D1 - Admitting a typed claim

1. same Context? If yes → check ⊑ (k ⊑ k′ if expected). If no → require KindBridge.
2. Scope coverage? Compute covers(TargetSlice).
3. Membership defined? MemberOf(?, k(′), TargetSlice) defined? If no → deny.
4. Bridges used? Apply penalties Φ/Ψ to R.
5. Freshness? Check windows. Optional: F ≥ F_k if ESG mandates.

D2 - Composing A → B

1. Typed: k_A ⊑ k_B or KindBridge to k′_B ⊑ k_B.
2. Scope: Scope(A) ∩ Scope(B) covers TargetSlice.
3. Penalties: apply Φ/Ψ to R.
4. Freshness: along serial path.
5. If mask expected: either A implies it or add mask adapter.

D3 - Union across lines

1. Prove per‑line typed admission.
2. Provide independence partition.
3. Publish SpanUnion; no extrapolation.

#Guard Anti‑patterns & Remedies (informative)

#Worked Examples (informative, brief)

Detailed scenarios remain in C.3 §11. This Annex sketches how the macros apply; cross‑reference as needed.

E1 — Safety braking policy (same Context). Use Guard_TypedClaim: PassengerCar ⊑ Vehicle passes; ClaimScope ∩ plant scopes covers TargetSlice; no bridges → no penalties; freshness checked.

E2 — Cross‑plant reuse (both bridges). Use Guard_XContext_Typed: Scope bridge (CL=2) narrows temp; KindBridge (CL^k=2) collapses EV subkind. Apply Φ(2)×Ψ(2) to R; publish loss notes.

E3 — API rule with adapter. Use Guard_TypedJoin: producer Request → consumer expects AuthenticatedRequest. Either prove ⊑ or add adapter; Scope remains separate (API v2.3 with Γ_time window).

E4 — Masked clinic cohort across jurisdiction. Use Guard_MaskedUse + Guard_XContext_Typed: registered mask, deterministic DOB constraint; KindBridge CL^k=1; Scope bridge CL depends on coding; penalties to R; Scope narrowed to overlap.

#Rationale (why an Annex) (informative)

• Focus. Keeps guard mechanics together, easing adoption in ESG/Method templates.
• Separation. Prevents leakage of AT/typed flavor into “Scope math”.
• Auditability. Standard shapes let reviewers check determinism, bridges, penalties, and freshness quickly.
• Inter‑pattern glue. Hooks USM, Kind‑CAL, Bridges, and F–G–R without inventing new scales.

#C.3.A:Annex A - How typed reasoning plugs into Compliance & Regulatory Alignment [A/I]

For managers. This section shows how to make regulatory adoption and reuse precise, auditable, and portable using Kinds, KindBridges (with a kind‑bridge congruence level, noted as CL^k for editors), and USM Scope. It cleanly separates what the law is about from where and when it applies, and routes any cross‑jurisdiction uncertainty to R (assurance). It never changes F (form) or G (scope) to hide mismatches.

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

What this solves. Regulations and standards name classes of things (“Adult person,” “Class II medical device,” “Personal data,” “Lease”). In one context they are native; in another they are foreign. Without typed reasoning, teams either (a) hand‑translate terms (silently changing meaning), or (b) reduce everything to Context labels (“domain = EU”), which cannot be checked by guards.

What we add.

1. Model regulatory categories as Kinds (with KindSignature and ⊑),
2. map them across Contexts with KindBridges and type‑congruence CL^k,
3. express Claim scope (G) over Context slices that explicitly list jurisdiction, version, and a time selector (Γ_time), and
4. apply R‑penalties (Ψ(CL^k)and, if scope is bridged,Φ(CL)) while keeping F and G unchanged.

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

Conformance. A model or authoring action conforms to A.2 iff it satisfies C‑REG‑1..C‑REG‑8 below.

C‑REG‑1 (Regulatory kinds). Regulatory categories SHALL be represented as U.Kind in the authority’s Context (e.g., AdultPerson@RegY, MedicalDeviceClassII@FDA, PersonalData@GDPR, Lease@IFRS). Each such kind SHALL have a KindSignature with a declared F level (C.3.2).

C‑REG‑2 (KindBridge). Cross‑context reuse of a regulatory category MUST declare a KindBridge with a kind‑bridge congruence level (CL^k) and loss notes (C.3.3). The mapping SHALL preserve the “is‑a / subkind‑of” direction and MUST NOT invert it.

C‑REG‑3 (Scope is USM). Regulatory applicability (jurisdiction, effective dates, product families, platforms) SHALL be expressed as Claim scope (G) over U.ContextSlice, with an explicit time selector (Γ_time). Applicability MUST NOT be encoded into kinds.

C‑REG‑4 (No synonym shortcuts). Editors MUST NOT treat legal terms as synonyms of local kinds without a KindBridge. Any term alignment SHALL be documented (mapping + CL^k + loss notes).

C‑REG‑5 (Determinism). MemberOf(e, k_reg, slice) MUST be deterministically evaluable when used in guards (no “latest law” or unstated grace periods).

C‑REG‑6 (Penalties land in R). When a claim or guard relies on Cross‑context classification (membership decided via a KindBridge), the receiving Context MUST apply the kind‑bridge penalty (based on CL^k) to R; if the Scope is also bridged, apply the scope‑bridge penalty (based on CL) to R as well. Invariant: penalty routing changes R only; F and G remain unchanged.

C‑REG‑7 (Editioning). Changes in law/regulator guidance that alter membership or applicability SHALL be recorded as content changes: update KindSignature (kinds) and/or update Claim scope (ΔG±). Guards MUST name a time selector (Γ_time) and MUST NOT rely on an implicit “latest” time.

C‑REG‑8 (Masks, not clones). Local process nuances (e.g., clinic‑specific cohort definitions) SHALL be captured with RoleMasks over the adopted kind; editors MUST NOT clone a new kind unless a stable subkind is warranted.

#C.3.A:A.3 Guard macros (ready to use)

(a) Guard_RegAdopt — adopt a regulatory requirement into a Context (Plain: check scope, map the legal category, and account for penalties)

Use when an internal policy is defined by reference to an authority’s category.

Inputs: Claim P (policy), RegKind k_reg in Context R_auth, TargetSlice S_local
Guard_RegAdopt(P, k_reg, S_local):
  1. ScopeCoverage:       U.ClaimScope(P) covers S_local                 // USM
  2. Γ_time:              S_local specifies Γ_time (no "latest")         // USM
  3. KindBridge:          a KindBridge exists that maps the legal category to a local kind, with **CL^k** at least the minimum policy level
  4. MemberOfDefined:     MemberOf(?, k_local, S_local) is defined       // determinism
  5. Penalties→R:         apply the **kind‑bridge penalty** (based on CL^k) to **R**
  6. ScopeBridge?         if the policy’s scope lives in the authority’s Context, translate it via a Scope Bridge; apply the **scope‑bridge penalty** (based on CL) to **R**
  7. EvidenceFreshness:   freshness windows for any bound evidence hold  // C.2.2

(b) Guard_RegChange — react to a regulatory change (Plain: re‑issue the kind and/or scope and refresh penalties)

Inputs: Reg change Δ (new edition, guidance), impacted kinds/claims
Guard_RegChange(Δ):
  1. Identify impact:      does Δ alter KindSignature (membership) or Scope predicates?
  2. If KindSignature:     version k_reg; update KindBridge; re-evaluate CL^k; update loss notes
  3. If Scope:             publish ΔG± (widen/narrow) to Claim scope; update guards
  4. Reassess penalties:   recompute Ψ(CL^k), Φ(CL) → R
  5. Γ_time discipline:    set sunrise/sunset; forbid implicit retroactivity in guards

(c) Guard_RegXContextUse — cross‑jurisdiction use with both bridges (Plain: move scope and kind, then account for both penalties)

Guard_RegXContextUse(P, k_reg@R_auth, S_local@R_local):
  1. Scope bridge:      a Scope Bridge from the authority Context to the local context exists with CL at least the policy minimum; the translated scope covers the local slice
  2. Kind bridge:       a KindBridge maps the legal category to a local kind with **CL^k** at least the policy minimum
  3. MemberOfDefined:   MemberOf(?, k_local, S_local) is defined
  4. Penalties→R:       apply the **scope‑bridge** and **kind‑bridge** penalties to **R**
  5. Loss-guided narrow: optionally narrow Scope' where known losses are material (best practice)

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

(1) Healthcare — “Adult” dosage rule across jurisdictions

Reg source. Jurisdiction Y defines AdultPerson@RegY (AT around K2, F4) with age at least 18; your hospital Context uses AdultPatient (age at least 21). Claim. “For all x ∈ AdultPatient: dosage ≤ D/kg for drug M.” Adoption.

• KindBridge. Map AdultPerson@RegY → AdultPatient; CL^k = 1; loss note: boundary mismatch (18↔21).
• Scope. {jurisdiction=Y, formulary=M, time selector (Γ_time)=from 2026‑01‑01}.
• Guard. Guard_RegAdopt passes; R penalized by Ψ(1). Policy narrows Scope to mapped cohort (age≥21) for in‑house use.
• Change. If Y changes adult to ≥19 (new edition), run Guard_RegChange: version the kind, refresh the bridge, re‑assess CL^k, update guards.

(2) Privacy — GDPR↔CCPA PII across Contexts

Reg kinds. PersonalData@GDPR, PersonalInformation@CCPA. Internal kind. PersonalData@Product with masks per data store. Policy claim. “No sharing of SensitiveAttribute outside processors.” Adoption.

• KindBridges. SensitiveAttribute@GDPR → SensitiveAttribute@Product (CL^k=2); SensitivePersonalInformation@CCPA → SensitiveAttribute@Product (CL^k=1, loss: biometric nuance).
• Scope. Two policies with SpanUnion over {jurisdiction=EU} and {jurisdiction=CA}, each with its own Γ_time windows and evidence freshness.
• Guards. For CA, apply stronger R penalty (Ψ(1)), and narrow to the mapped subset (exclude ambiguous fields).
• Do not. Do not rename GDPR terms to local labels without a KindBridge.

(3) Export control — US EAR “600‑series” classification

Reg kind. EAR600SeriesItem@US (AT≈K2, F3→F4 as predicates are formalized). Local kind. Product@Company. Work scope. {destination=countries, end_use, time selector (Γ_time)=shipment date} for the shipping capability. Adoption.

• KindBridge. Map EAR600SeriesItem@US → Product@Company; CL^k=2 (loss: component kit edge cases); loss notes recorded.

• Capability guard (Method–Work).

  • U.WorkScope(Ship) covers JobSlice (destination, end use, time).
  • MemberOf(product, EAR600_mapped, JobSlice) defined (classification present).
  • Apply Ψ(2) to R (classification uncertainty) and, if reusing US scope text, Φ(CL_scope) too.

• Outcome. Shipment admitted only for allowed destinations; higher R may require manual review.

(4) Finance — IFRS vs US GAAP “Lease”

Reg kinds. Lease@IFRS, Lease@USGAAP. Local kind. LeaseStandard@Corp used in policy “recognize lease liabilities.” Adoption.

• KindBridge. Lease@IFRS → LeaseStandard@Corp (CL^k=2; loss: short‑term exceptions differ).
• Scope. {jurisdiction=IFRS, Γ_time=financial period, ledger=v7}.
• Evidence. LA plans cover subkinds (operating vs finance) per your classification; the kind‑bridge congruence level (CL^k) drives extra testing near boundary cases.

#C.3.A:A.5 Design guidance & pitfalls [I]

Do this.

• Treat regulatory categories as Kinds. Put the definition into KindSignature (aim for F4 predicates where practical).
• Make time explicit. In guards, require a time selector (Γ_time) for effective dates and grace periods. Forbid “latest”.
• Publish bridges with loss notes. If two jurisdictions’ categories are “almost the same,” say how, rate CL^k, and note what is lost.
• Split “where” from “what.” Keep Scope (G) over U.ContextSlice (jurisdiction, plant, Standard versions) separate from MemberOf on the kind.
• Route uncertainty to R. Use Ψ(CL^k) and Φ(CL); never modify F/G to hide ambiguity.

Avoid this.

• Synonym games. Don’t alias “Adult” to local AdultPatient in prose. Use a KindBridge.
• Scope by labels. “Domain = EU” is not a guard. Use explicit U.ContextSlice fields (jurisdiction, version, time selector) and Scope predicates.
• Hiding time. Never rely on “current law”; always fix Γ_time (point/window/policy).
• Widening G to compensate for type gaps. If kinds don’t line up, introduce a subkind, add a mask/adapter, or narrow; don’t “make the scope bigger”.

#C.3.A:A.6 Migration checklist [I]

1. Inventory regulatory references in policies/specs.
2. Create Kind cards for referenced legal categories (intent summary, KindSignature + F, known subkinds, AT tag if helpful).
3. Publish KindBridges to your local kinds with CL^k and loss notes.
4. Rewrite guards to use Scope coverage (USM) plus MemberOf on the mapped kind; add an explicit time selector (Γ_time).
5. Wire penalties: Ψ(CL^k) and Φ(CL) lower R; refresh evidence windows.
6. Catalog RoleMasks for local nuances; promote frequently reused masks to subkinds.

#C.3.A:A.7 Manager’s one‑page pattern [I]

• Question 1 — Where does the rule apply? → Scope (G) over Context slices (jurisdiction, plant, Standard, and a time selector (Γ_time)).
• Question 2 — About what things? → Kind (regulatory category) with a KindBridge if foreign.
• Gate recipe. Scope covers the TargetSlice and membership for the mapped kind is defined, and both bridges are present where needed; then apply bridge penalties to R and decide.
• Change handling. New law edition? Update KindSignature/Bridge (kinds) and/or Scope (ΔG); never rely on “latest.”
• Accountability. Keep loss notes, CL/CL^k, and Γ_time in the decision record.

#C.3.A:Annex B - How typed reasoning plugs into Assurance Lanes (VA/LA/TA) & Evidence design [A/I]

Intent (manager’s view). Typed reasoning turns “prove/test/qualify” into a repeatable plan. By making what the rule talks about explicit (named Kinds, their subkinds, and optional RoleMasks), you can:

1. design proof obligations that actually quantify over the right things (VA),
2. build test plans that cover the right variants/subkinds in the right context slices (LA), and
3. isolate tool risk (TA) instead of letting it bleed into scope or type semantics.

Invariant reminders. — Scope (G) is where a claim holds — expressed over U.ContextSlice (with an explicit time selector, Γ_time). — Kind membership is which things the claim ranges over inside that slice — checked with MemberOf(… , kind, slice). — Bridge penalties: the scope‑bridge penalty (based on CL) and the kind‑bridge penalty (based on CL^k) both lower R (assurance). They never change F (form) or G (scope).

#C.3.A:B.1 What you get with typed assurance [I]

• Targeted proofs (VA). If a policy says “for every PassengerCar …” (notation hint: ∀x:PassengerCar), the VA lane now has a clear target. You can prove obligations once for the kind (and its subkinds), instead of re‑proving per ad‑hoc label.
• Subkind‑aware test plans (LA). Test matrices are indexed by subkinds (and RoleMasks) × context slices; coverage stops being accidental.
• Deterministic guards. A test/proof either applies to the TargetSlice and Kind (Scope covers & MemberOf defined) or it doesn’t. No “latest,” no silent widening.
• Clean tool boundaries (TA). You qualify the prover/model‑checker/classifier once and route tool confidence to TA, not to “broadened” claims.

#C.3.A:B.2 Normative obligations for evidence design

EA‑1 (Two checks). Every VA/LA artifact that supports a typed claim SHALL bind both:

• Scope predicate: U.ClaimScope(Claim) covers TargetSlice (with explicit Γ_time), and
• Kind predicate: MemberOf(?, k, TargetSlice) is defined (deterministic).

EA‑2 (Subkind coverage). When a claim quantifies over k, target‑contexts SHALL justify LA coverage per relevant subkind of k (or per RoleMask if masks stand in for stable subkinds). “Representative set” MUST be stated explicitly.

EA‑3 (Independence for unions). If a published SpanUnion of evidence lines is used to enlarge covered area, independence of lines SHALL be documented (no shared weakest link).

EA‑4 (Bridges accounted). If a VA/LA artifact travels across Contexts:

• Scope movement SHALL use a Scope Bridge (Part B) with CL and apply the scope‑bridge penalty to R.

• Kind movement SHALL use a KindBridge (§ C.3.3) with CL^k and apply the kind‑bridge penalty to R. Neither movement SHALL alter F or G.

  Neither movement SHALL alter F nor G.

EA‑5 (Freshness). LA evidence SHALL declare freshness windows tied to Γ_time (no implicit “latest”). Expiry MUST fail guards closed until refreshed.

EA‑6 (No scope‑by‑wording). Editors MUST NOT widen G by rewriting a claim to sound “more general.” Widening G (ΔG+) is permitted only with new support that truly enlarges the set of slices.

EA‑7 (TA separation). Tool qualification (TA) SHALL be tracked independently. VA/LA guards MUST NOT substitute “tool is trusted” for content proof/coverage.

#C.3.A:B.3 Designing the evidence matrix [I]

A practical way to plan LA/VA is a matrix:

| Row set | Column set | Cell content |

| ----------------------------- | ------------------------------------------------------------ | ---------------------------------------------------------------------------------------------------------------------- | | Kinds (subkinds or masks) | Context slices (Standard versions, env ranges, Γ_time) | Evidence unit (proof fragment, test batch, monitoring window), with Scope and MemberOf predicates attached |

• Choose rows. Start with the kind and list relevant subkinds (notation hint: kᵢ is a subkind of k) or stable RoleMasks.
• Choose columns. Split your declared Scope (G) into named slices you intend to support (e.g., “dry, speed up to 50” and “wet, speed up to 40” with specific rigs and versioned Standards).
• Fill cells. Attach one or more evidence units per cell (proof obligations for VA; test campaigns/monitoring windows for LA). Mark bridged cells and their CL/CL^k penalties to R.

Tip. For formal kinds and “up‑to‑iso” kinds (AT K2/K3), expect more rows (more variants to cover). For instance‑like kinds (AT K0), expect fewer rows and tighter columns (narrow slices, stricter freshness).

#C.3.A:B.4 VA lane — proofs that match the kind [A/I]

What VA contributes. Proofs reduce ambiguity and eliminate many LA burdens when they truly quantify over the intended kind and live in the declared Scope.

VA‑patterns (informative):

• Proof over the Kind (F7–F8). “For every PassengerCar, the property holds” (notation hint: ∀x:PassengerCar). If the property depends on subkind‑specific rules, split lemmas per subkind.
• Proof‑carrying components. When the content is F8 (dependent types), the build rejects violations; LA can shrink to conformance smoke within the slices.
• Up‑to‑iso (AT K3). Equational reasoning “up‑to‑iso” is acceptable only if the KindSignature works at that level and receivers accept KindBridge that preserves equivalences.

VA‑obligations (normative):

• VA‑1. A proof artifact SHALL cite the Kind it quantifies over and reference the Claim scope slices it assumes.
• VA‑2. Cross‑context acceptance of proofs SHALL use both bridges (Scope+Kind) and apply Φ/Ψ penalties to R (never to F/G).
• VA‑3. If the proof relies on tool kernels, their TA status SHALL be disclosed; weakening TA MUST NOT be “paid for” by silent scope widening.

Mini‑example (VA). Policy P: “∀ x: PassengerCar. stoppingDistance(x) ≤ 50 m on dry at speed≤50.” — Kind: PassengerCar ⊑ Vehicle (K2), signature F4 (predicates). — Scope: {surface=dry, speed≤50, rig=v3, Γ_time=rolling 180 d}. — Proof: a proof assistant lemma over PassengerCar (tool choice is context‑local). — Reuse to Plant‑B: a Scope Bridge with CL=2 (rig bias) and a KindBridge with CL^k=3 (same classification). Apply the scope‑bridge penalty for CL=2 and the kind‑bridge penalty for CL^k=3 to R.

#C.3.A:B.5 LA lane — tests & monitoring that cover the right variants [A/I]

What LA contributes. Empirical assurance for claims with executable semantics or physical interfaces; especially when F ≤ F6 or when stochastic/real‑world effects matter.

LA‑patterns (informative):

• Cover by subkind. Test at least one representative per subkind; add more where variability inside a subkind matters.
• Boundary probing. Concentrate tests near KindSignature and Scope boundaries (e.g., temp limits, speed caps).
• Hybrid checks (F6). When software controllers interact with physical systems, ensure both sides declare obligations; include their interaction cases in the matrix.
• Monitoring windows. For live systems, define Γ_time policies (e.g., rolling 30 d) and tie alerts to kind‑aware metrics (“error rate per ServiceInstance”).

LA‑obligations (normative):

• LA‑1. Each test campaign SHALL specify rows/columns in the evidence matrix and attach Scope/MemberOf predicates to each run.
• LA‑2. Freshness windows SHALL be explicit and enforced in guards (no “latest”).
• LA‑3. If a KindBridge merges subkinds, test plans SHALL be adjusted (more cells, stricter acceptance), and the kind‑bridge penalty (based on CL^k) applied to R.
• LA‑4. Publishing SpanUnion coverage requires the independence note (which support lines differ).

Mini‑example (LA). Claim: “For all x ∈ Vehicle: brakeDistance ≤ 50 m on dry, ≤ 40 m on wet.” — Rows: {PassengerCar, LightTruck}. — Columns: {dry, ≤50}, {wet, ≤40} with rigs and versions. — Cells: PC/dry covered by track tests; LT/wet by simulation + surrogate tests (independent lines → SpanUnion allowed). — Bridge to jurisdiction Y collapses EV vs ICE ⇒ CL^k=2. Apply Ψ(2) to R; add extra wet tests to compensate.

#C.3.A:B.6 TA lane — tool qualification where it belongs [A/I]

What TA contributes. Confidence in provers, checkers, model‑checkers, data classifiers and pipelines. TA is about the machinery, not the claim or kind semantics.

TA‑patterns (informative):

• Prover kernels. Audit/qualification of the kernel version used for VA proofs.
• Automated Model‑checkers. Qualification against seeded faults; document limits (precision, nondeterminism).
• Classifiers used for MemberOf. If membership uses ML or rules engines, qualify the classifier separately; any drift monitoring belongs to LA freshness.

TA‑obligations (normative):

• TA‑1. Tools critical to VA/LA SHALL declare their qualification status and version; guards SHALL reference these declarations when they matter. TA‑2. Lower tool qualification MUST NOT be hidden by relaxing F or widening G. target‑contexts may offset it by demanding more evidence in R (for example, extra tests), per policy.

#C.3.A:B.7 Guard macros for evidence planning & attachment

Guard_EvidencePlan_Typed — approve a plan that is adequate for a typed claim. Plain reading. The first macro checks that the plan names the rows (kinds or masks) and columns (slices), that scope and membership can be checked for each cell, that any Cross‑context moves declare bridges, and that penalties are budgeted in R.

1. MatrixDeclared:    Evidence matrix rows = {subkinds or masks of k}; columns = {TargetSlices within ClaimScope}
2. ScopeBound:        For each column, ClaimScope covers that slice with explicit Γ_time
3. KindBound:         MemberOf(?, k, slice) is defined (deterministic) for all planned slices
4. BridgeBudgeted:    If cross-context:
                        (a) Scope Bridge(s) declared with CL → attach the **scope‑bridge penalty** to the **R** budget
                        (b) KindBridge(s) declared with CL^k → attach the **kind‑bridge penalty** to the **R** budget
5. FreshnessPolicy:   LA freshness windows specified per slice; monitoring plan defined (if live)
6. IndependenceNote:  If SpanUnion is claimed, independence justification attached
7. TADecls:           Tools and their TA status listed; residual risk routed to R (not to F/G)

Guard_EvidenceAttach_Typed — attach concrete evidence to a state change. Plain reading. The second macro checks that each attached evidence unit clearly states which row and column it covers, binds scope and membership in a reproducible way, applies bridge penalties to R, and respects freshness.

1. CellMatch:         Each evidence unit cites (subkind/mask, slice) it covers
2. PredicateBinding:  Evidence embeds Scope and MemberOf predicates (or references them verifiably)
3. BridgeApplied:     If evidence is bridged, apply the **scope‑bridge** and/or **kind‑bridge** penalties to **R**; record loss notes
4. FreshnessMet:      Evidence within declared freshness; else guard fails closed
5. VA/LA Mix:         If VA present, verify it matches the quantified Kind; if LA fills gaps, show matrix deltas
6. TAConsistent:      Tool versions match TA declarations used at planning time

#C.3.A:B.8 Anti‑patterns & remedies

#C.3.A:B.9 End‑to‑end example (manager’s cheat‑sheet) [I]

Scenario. You want to publish “∀ x: PassengerCar. brakeDistance ≤ 50 m dry; ≤ 40 m wet” across two plants.

1. Kinds. PassengerCar ⊑ Vehicle (K2, signature F4).
2. Scope (G). {surface in {dry, wet}, speed limits, rig version, time selector (Γ_time)=rolling 180 days} in Plant‑A.
3. VA. Prove the property for PassengerCar using a proof assistant, and cite the Scope slices it assumes.
4. LA. Build an evidence matrix with rows {PassengerCar} and columns {dry, up to 50} and {wet, up to 40}, including rig variants; add boundary tests near the limits.
5. TA. Qualify the prover kernel and the automated checker used for wet surrogates.
6. Bridge. To Plant‑B: a Scope Bridge with CL=2 (rig bias) and a KindBridge with CL^k=3 (same classification).
7. Penalties. Apply the scope‑bridge penalty for CL=2 and the kind‑bridge penalty for CL^k=3 to R. Per policy, add extra test cells in Plant‑B to compensate for rig bias.
8. Guards. Use Guard_EvidenceAttach_Typed on the state change; include freshness checks.

Outcome. A defensible, auditable publication: typed, scoped, with clear evidence coverage and explicit risk penalties — no conflation of abstraction with applicability, and no tool risk smuggled into content.

#C.3.A:Annex C. ESG guards

Status note. This profile restates the guard semantics from §4 for ESG/Method contexts. It does not add obligations; where wording diverges, §4 controls.

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

When a state transition publishes or affirms a claim that quantifies over kinds, the guard SHALL:

1. Scope coverage (USM). U.ClaimScope(Claim) covers TargetSlice (singleton or finite set) and TargetSlice declares Γ_time (no “latest”).

2. Typed definedness. A deterministic membership check is available for every kind used by the claim in the TargetSlice. If membership cannot be evaluated in that context, the guard fails closed.

3. Typed compatibility (same Context). If a downstream consumer expects a specific kind, then for each kind used by the claim either:

• the used kind is an is‑a / subkind‑of the expected kind, or
• a documented RoleMask for the expected kind is used and its constraints are met and observable in the TargetSlice.

3. Typed compatibility (Cross‑context). If any referenced kind is used across Contexts, a KindBridge SHALL be declared with a published type‑congruence level (minimum acceptable level per Context policy), order preserved (no inversions), and loss notes.
   The guard SHALL apply the kind‑bridge penalty to R.

4. Scope translation (Cross‑context claim use). If the Claim’s scope originates in another target‑context, a Scope Bridge with a published congruence level is required; apply the scope‑bridge penalty to R.

5. Formality threshold (if gated). If the ESG state requires rigor, enforce U.Formality(Claim) ≥ F_k (C.2.3). (Note: Raising F does not widen G; do not substitute.)

6. Evidence freshness (R). Where the new state implies trust, assert freshness windows and confirm no expired bindings.

Prohibitions (normative).

• Do not widen G to “hide” a type mismatch. Fix typed compatibility (introduce a subkind, use a RoleMask, publish a KindBridge) or reject.
• Do not treat a mask name as a kind—masks must be registered and deterministic.
• Do not infer G from the size of a kind’s Extension; Scope ≠ Extension.

#Method–Work guard obligations (normative)

To admit a capability for a specific Work step at JobSlice, the guard SHALL:

1. Work scope coverage (USM). The capability’s Work scope covers the JobSlice, and the JobSlice includes an explicit time selector (Γ_time).

2. Measures & qualification. All required U.WorkMeasures hold at JobSlice and the U.QualificationWindow is valid at Γ_time.

3. Typed inputs (same Context). For each declared input kind (or RoleMask), assert:

   • Membership check available: the system can deterministically decide whether the input belongs to the expected kind in this JobSlice.
   • Compatibility: the provided input kind is an is‑a / subkind‑of the expected kind, or the RoleMask constraints are satisfied and observable.

4. Typed outputs / post‑conditions (if declared). If the capability guarantees an output kind k_out, record the obligation to demonstrate MemberOf(output, k_out, JobSlice) (typically via conformance tests or audits).

5. Cross‑context typed use. If inputs/outputs are typed in a different target‑context than the capability or JobSlice:

   • KindBridge(s) are required with a published type‑congruence level and loss notes; apply the kind‑bridge penalty to R.
   • If the capability resides in another target‑context, a Scope Bridge with a published congruence level is required; apply the scope‑bridge penalty to R.

6. No substitution by G. Do not “fix” a typed mismatch by widening the Work scope. Use an adapter or a RoleMask, or reject.

#Guard macros (ready‑to‑use)

ESG_TypedGate(Claim, TargetSlice, Kinds, thresholds) Manager view: The following macros are for editors; target‑contexts may automate them if desired. Managers can read the comments on each step; the checks are the same ones described in Plain language above.

1  assert ClaimScope(Claim) covers TargetSlice                 // USM
2  assert Γ_time(TargetSlice) is explicit                  // no "latest"
3  for each kind k in Kinds used by Claim:
4      assert membership_defined(k, TargetSlice)               // C.3.2 K-07
5  if same-Context typed expectations exist:
6      assert is_subkind(k, k_expected) OR meets_mask_constraints(k_expected, TargetSlice)
7  if cross-context kinds:
8      assert KindBridge(k, k') with type_congruence ≥ c_kind and loss notes
9      apply_kind_bridge_penalty(type_congruence)
10 if cross-context scope:
11     assert ScopeBridge(Claim.Context, TargetSlice.Context) with congruence ≥ c_scope
12     apply_scope_bridge_penalty(congruence)
13 if F-threshold applies: assert Formality(Claim) ≥ F_k        // C.2.3
14 if trust implied: assert Fresh(evidence, window) AND NoExpiredBindings

MethodWork_TypedGate(Capability, JobSlice, Inputs/Outputs, thresholds)

1  assert WorkScope(Capability) covers JobSlice                // USM
2  assert Γ_time(JobSlice) is explicit
3  assert WorkMeasures(JobSlice) satisfied AND QualificationWindow holds
4  for each expected input-kind k_in:
5      assert membership_defined(k_in, JobSlice)
6      assert is_subkind(k_input, k_in) OR meets_mask_constraints(k_in, JobSlice)
7  if declared output-kind k_out: record obligation to show MemberOf(output,k_out,JobSlice)
8  if cross-context kinds: assert KindBridge(… ) with type_congruence ≥ c_kind; apply_kind_bridge_penalty(type_congruence)
9  if cross-context capability/scope: assert ScopeBridge(… ) with congruence ≥ c_scope; apply_scope_bridge_penalty(congruence)

#Worked examples (manager‑focused)

(A) ESG — Promote a braking policy to Effective. Claim. “For all vehicles: braking distance is ≤ 50 m on dry and ≤ 40 m on wet.” TargetSlice. {surface∈{dry,wet}, speed≤50 km/h, rig=v3, Γ_time=rolling 180 d} Kinds. Vehicle (K2, KindSignature at F4); the consumer subsystem expects PassengerCar. Guard.

1. Scope covers TargetSlice (USM ✓).
2. Definedness of MemberOf(?, Vehicle, TargetSlice) ✓.
3. Typed compatibility: PassengerCar ⊑ Vehicle ✓.
4. No bridges → no penalties.
5. F‑threshold: Formality(Claim) ≥ F4 ✓.
6. Freshness: evidence ≤ 180 days ✓. Result: Transition allowed. F/R apply weakest‑link on support paths; G remains the set declared.

(B) Method–Work — Admit “RiskScore” step with typed input. Capability. ComputeRiskScore expects AuthenticatedRequest; promises SLOs (latency ≤ 50 ms, error ≤ 0.5 %). JobSlice. {api=v2.3, region=eu‑west, Γ_time=now, traffic_class=gold} Inputs. Producer emits Request (no auth guarantee). Guard.

1. Work scope covers JobSlice; Measures & QualificationWindow ✓.
2. Typed inputs: MemberOf(?, AuthenticatedRequest, JobSlice) must hold. Not true for raw Request.
3. Remedy: insert an adapter that enforces/attests auth → yields AuthenticatedRequest.
4. No Cross‑context → no bridges. Result: Admitted with adapter; Scope unchanged; R relies on adapter evidence. Widening Work scope is not acceptable to bypass typed mismatch.

(C) Cross‑context ESG — Adopt policy across plants. Claim Context. SafetyLab@2026. target Context. PlantB@EU. Kinds. Vehicle ↦ TransportUnit via KindBridge with CL^k=2 (EV/ICE collapsed); Scope Bridge from lab to plant with CL=2 (rig bias ±2 %). Guard.

1. Translate Scope and cover TargetSlice_B.
2. Translate Kind and ensure MemberOf(?, TransportUnit, TargetSlice_B) is defined.
3. Apply the scope‑bridge penalty (level 2) and the kind‑bridge penalty (level 2) to R; publish loss notes. Result: Transition allowed with reduced R; G is the mapped set; F unchanged.

#Anti‑patterns & remedies (normative where noted)

#C.3.A:End