#C.3:7.1 How typed reasoning plugs into F–G–R & USM

Preface node heading:c-3-7-1-how-typed-reasoning-plugs-into-f-g-r-usm:32120

#Content

#The basic shape of a typed claim (manager view)

A typed claim has two independent parts:

1. describedEntity (Kind). Which things the statement talks about. “For every item of kind k in the target context (the selected TargetSlice) …”. — The definition of kind k lives in KindSignature(k) (with its F, C.3.2). — Which items count as “k” is evaluated in the TargetSlice (C.3.2) by a deterministic membership check.

2. Applicability (Scope, G). Where the statement holds. U.ClaimScope(Claim) is the collection of contexts where the claim is valid (USM A.2.6). Guards test: “Scope covers the TargetSlice”.

Discipline. The guard first checks typed compatibility (in the same Context: “is‑a / subkind‑of”; across Contexts: a KindBridge, C.3.3), then Scope coverage (USM), then R freshness and any bridge congruence penalties. See C.3.A Guard_TypedClaim.

#Composition of typed claims

Rule C‑T‑1 (typed pre‑check). To compose a producer claim with a consumer claim, where the producer quantifies over kind k (source) and the consumer expects kind k (expected):

• same Context: require “is‑a / subkind‑of” to hold (the source kind is a subkind of the expected kind) (C.3.1).

• Cross‑context: require a KindBridge that maps the source kind to a local kind that is a subkind of the expected kind in the target Context (C.3.3). If neither holds, the composition is unsafe; introduce a subkind, add an adapter (or a RoleMask), or decline.

• Role‑aware option (same Context): if the consumer expects a RoleMask over the expected kind, you may satisfy the mask’s explicit constraints (C.3.4) instead of changing kinds, provided those constraints are observable at gate time.

Rule C‑T‑2 (scope after type). After typed compatibility is satisfied, compute Scope as in USM:

• Serial path: take the intersection of the contributors’ claim scopes.
• Parallel independent lines: use SpanUnion of the serial scopes (only if independence is justified).

Rule C‑T‑3 (no type‑by‑scope). A kind mismatch MUST NOT be “fixed” by widening G. Changes in describedEntity require subkind introduction, signature edits, or a KindBridge—not a scope change.

Manager hint. First confirm the port shape matches (kinds line up), then check the operating area (scope), and finally look at confidence (evidence freshness plus any bridge congruence penalties).

#F–G–R with typed claims (what changes, what doesn’t)

• F (Formality). – Claim‑level F follows C.2.3 (weakest‑link along the claim’s support paths). – KindSignature F is declared on the kind (C.3.2) and influences claims only if the claim essentially depends on those predicates (weakest‑link again). – Raising F can reveal hidden assumptions (which may trigger ΔG in the claim), but does not change G by itself.

• G (Scope). – Always set‑valued over Context slices (USM A.2.6). – Typed reasoning does not alter G’s algebra (∈/∩/SpanUnion/translate). – Never infer Scope from “how general the wording sounds.”

• R (Reliability). – Evidence freshness/decay (validation windows) remains separate from Scope coverage. – Cross‑context penalties split cleanly: a scope‑bridge penalty (USM) and a kind‑bridge penalty (C.3.3). Both reduce R only; neither changes F or G.

Manager rule of thumb. Start with the reliability from your support; then apply the scope‑bridge penalty; then apply the kind‑bridge penalty. Each step can only reduce reliability.
You never add or average F/G: you compose scope per USM rules and apply weakest‑link for F/R along support paths.

#ESG gating with typed claims

• Gate on F, if your Context requires rigor before use (e.g., U.Formality(Claim) ≥ F4).
• Gate on Scope coverage (USM) and an explicit time selector (Γ_time) policy.
• Gate on R freshness and minimum congruence for bridges (e.g., CL ≥ 2, CL^k ≥ 2).
• Do not gate on AT (C.3.5); it is an informative facet only.
• Use C.3.A guard macros to keep guards short and auditable.

#How typed reasoning plugs into the CAL chain (Lang‑CHR → Role‑CAL)

Intent. Show a clear, end‑to‑end path a manager can follow to take a typed claim from words to safe reuse across Contexts—without any tool or data‑governance assumptions. Each stage says what it supplies, what it needs, and what it hands off to the next stage.

#Lang‑CHR — stable words first

What it supplies. A disciplined vocabulary and controlled phrasing so that terms like Vehicle, AuthenticatedRequest, AdultPatient have one meaning in the Context.

What it requires. Authors use controlled narrative (C.2.3 F3) at minimum: single‑meaning terms, explicit “shall / if / then”, and no drifting synonyms.

Hand‑off. A small, curated lexicon entry for each candidate Kind‑word; these become U.Kind names in the next step.

Manager hint. If two teams cannot agree on the noun, you are not ready to type the claim. Resolve the noun in Lang‑CHR before introducing a Kind.

#Kind‑CAL (this Part) — name the describedEntity

What it supplies. • U.Kind objects for those nouns; a partial order ⊑ (subkind‑of). • KindSignature(k) (intent), with declared F. • Extension(k, slice) and MemberOf(e,k,slice) (extent). • (Optional) AT (K0…K3) as an informative facet.

What it requires. • Deterministic membership (no “latest” defaults) and a clear rule for where membership is defined in each context. • No “Kind scope”: Scope remains with claims/capabilities (USM).

Manager hint. Use the kind’s AT tag only as a planning signal (where to invest rigor and tests). AT never gates decisions and never widens scope.

Hand‑off. Typed quantifier sites for claims: “∀ x ∈ Extension(k, slice) …”, plus a visible ⊑ lattice for compatibility checks down the line. Typed claim sites written in Plain language: “for every item of kind k in the target context …”, plus a visible subkind‑of lattice for compatibility checks down the line.

Manager hint. Decide early whether your Kind is K0 (instance‑ish) or K2 (formal class). It sets your ΔF/ΔR budget expectations.

#Structure‑CAL — give Kinds usable shape

What it supplies. Structural building blocks on Kinds: • combinations (“and”), • alternatives (“either/or”), • records (named fields), • functions (inputs to outputs), plus relations like has‑attribute and part‑kind, and the minimal invariants those structures must respect.

What it requires. • Do not hide Scope inside structure. • Put structural rules into the KindSignature as checkable statements (ideally F4+).

Hand‑off. Typed ports and shapes of claims/specifications (“this policy expects PassengerCar × ControllerConfig”), making compatibility checks crisp before any Scope math.

Manager hint. If two claims expect different shapes (for example, one needs “Vehicle with ABS”, the other just “Vehicle”), plan a subkind or an adapter. Do not “solve” it by rewording the claim.

Note (informative). If a Context declares structural constructors on kinds (e.g., product/sum/record/function), editors SHOULD document the corresponding Extension inclusion laws for those constructors. Keep Scope in USM; do not hide it in structure.

#Compose‑CAL — compose with typed pre‑checks

What it supplies. The order of checks you must follow for safe composition:

1. Typed compatibility: in the same Context, the producer’s kind is a subkind of the consumer’s kind; across Contexts, a KindBridge maps the producer’s kind to a local kind that fits, with an acceptable kind‑bridge congruence level (C.3.3).
2. Scope checks (USM): along dependency paths, take the intersection of scopes; use SpanUnion only when support lines are truly independent.
3. Assurance wiring: apply the scope‑bridge penalty and the kind‑bridge penalty to R; check evidence freshness separately.

What it requires. Independence justification for SpanUnion; no “type‑by‑scope” fixes.

Hand‑off. A typed, scope‑checked composition that survives audit because each risk is accounted for in R.

Manager hint. Run the typed pre‑check first. It is the cheapest failure to catch and prevents “scope gymnastics” that mask a type mismatch.

#CT2R‑LOG — speak the logic, keep the math honest

What it supplies. • A clear logical reading of your typed claim: “for every item of kind K, condition φ holds” (or “there exists an item …”). • Rules for refinement and substitution that respect the subkind‑of relation. • When appropriate (K3), reasoning that treats structures as equivalent up to isomorphism (useful where exact identity is the wrong notion).

What it requires. • Pick a logic that matches the Formality you declare (e.g., machine‑checked logic for higher F). • When the logic travels across Contexts, use a KindBridge to keep meaning aligned; any mismatch is reflected as a kind‑bridge penalty in R.

Hand‑off. Proof obligations or reasoning templates that are consistent with your Kind/Structure setup and do not alter G. Shall‑note CT2R‑1. Transferring typed formulas that depend on MemberOf across Contexts uses a KindBridge; any mismatch is accounted as Ψ(CL^k) in R. F and G remain unchanged. For up‑to‑iso situations, see C.3.5 (AT) for when K3 is appropriate.

Manager hint. If your proof keeps failing when you move between Contexts, add a bridge at the Kind level; do not try to “fix” it by changing scope.

#Role‑CAL — adapt without cloning

What it supplies. RoleMask(kind, Context): a named, registered adaptation (extra constraints or local aliases, with optional narrowing) that reuses the same kind instead of creating a new one.

What it requires. • Constraints must be testable at gate time and give deterministic answers. • If a constraint mask is reused often, promote it to a subkind.

Hand‑off. Context‑specific views that keep identity intact and make typed guards practical (“use PaymentAccount@PCI mask in these steps”).

Manager hint. If the same mask appears in several guards, promote it to a subkind. This reduces future bridge and audit effort.

#Mini end‑to‑end example (manager‑oriented)

Scenario. A risk gate for API requests must be reused by another program across Contexts.

Lang‑CHR. Settle on Request, AuthenticatedRequest, RiskScore, BudgetSlack; write them in controlled phrases (F3).

Kind‑CAL. • Define Kind Request (K2) and a subkind AuthenticatedRequest ⊑ Request; publish a KindBridge for the PCI taxonomy with kind‑bridge congruence level 2 (loss note: token class is collapsed). • Membership MemberOf(e, AuthenticatedRequest, slice) is deterministic under API v2.3 and Γ_time policy.

Structure‑CAL. • AuthenticatedRequest is a record kind with fields (headers, tokenProof, body); invariants relate tokenProof to headers.

Compose‑CAL. • Policy P says in Plain terms: “for every AuthenticatedRequest in the target context, deny the call when riskScore is at or above the set risk threshold and budgetSlack is at or below the set budget limit.” • Another service S expects PCIRequest. Typed pre‑check: does AuthenticatedRequest ⊑ PCIRequest? No. • Remedy: adapter A proves AuthenticatedRequest → PCIRequest in this Context; if reusing across Contexts, publish a KindBridge for the PCI taxonomy with CL^k=2 (loss: token class collapsed).

CT2R‑LOG. • State P in a state P in a proof‑checked logic (where appropriate for F7+), so that changes to token rules break proofs. Proofs rely on the AuthenticatedRequest definition, not on the consumer’s scope.

Role‑CAL. • Register a RoleMask over PCIRequest for the consuming team; guards must be able to test the mask’s constraints at gate time.

Outcome. • Typed guard approves only when: (i) the type pre‑check passes (same‑Context subkind‑of or a KindBridge with an acceptable congruence level), (ii) Scope covers the target context (API v2.3, explicit time selector), and (iii) R reflects the scope‑bridge and kind‑bridge penalties and evidence is fresh. • No one widened Scope to hide a type mismatch; the adapter + bridge made the semantics explicit and auditable.

Takeaway. If you keep these six hand‑offs in view—words → kinds → structure → composition → logic → roles—you get predictable reviews, clean risk accounting, and reusable claims that travel across Contexts without silent meaning drift.

#Compliance & Regulatory Alignment — profile

Treat regulatory categories as Kinds, carry their intent in KindSignature with declared F, move them across Contexts with a KindBridge (type‑congruence CL^k + loss notes), and express applicability as Claim scope over U.ContextSlice (with explicit Γ_time). Any Cross‑context uncertainty is routed to R via Ψ(CL^k) (kind) and Φ(CL) (scope); F and G remain unchanged.

Authoritative obligations and guard macros (C‑REG‑1…8, Guard_RegAdopt / Guard_RegChange / Guard_RegXContextUse) and worked scenarios live in C.3.A, Annex A (Regulatory adoption profile).

#How typed reasoning plugs into Assurance Lanes (VA/LA/TA) & Evidence design

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, optional RoleMasks) and keeping Scope (G) over U.ContextSlice separate from membership inside the slice. Cross‑context uncertainty (Scope Bridge CL, KindBridge CL^k) always routes to R as penalties Φ/Ψ; it never changes F or G.

Evidence matrix (sketch).

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

Authoritative evidence obligations and guard macros (planning/attachment, VA/LA/TA duties, anti‑patterns) are in C.3.A, Annex B.

#How typed reasoning plugs into ESG and Method–Work gating

Intent. Make state changes and work admissions deterministic, auditable, and safe by separating (1) typed compatibility (what the statement or capability is about) from (2) scope coverage (where it holds or can run). Any Cross‑context uncertainty is routed to R (reliability) only—never to F (form) or G (scope).

#Scope & fit

This subsection defines normative guard obligations for:

• ESG (Episteme State Graph) transitions whose assertions quantify over kinds, and
• Method–Work admissions where a capability expects inputs/outputs of specified kinds.

It reuses:

• USM (A.2.6): U.ClaimScope (G) and U.WorkScope coverage + Γ_time,
• Kind‑CAL core (C.3.1–C.3.2): U.Kind, MemberOf(e,k,slice), ⊑,
• KindBridge (C.3.3) with CL^k and loss notes,
• Scope Bridge (Part B) with CL and loss notes,
• RoleMask (C.3.4) when local adaptations of a kind are used,
• Formality F (C.2.3) when transitions gate on rigor,
• Assurance R (C.2.2) for evidence freshness and penalties Φ/Ψ.

Guard macros. The normative guard shapes for ESG and Method–Work (Guard_TypedClaim, Guard_TypedJoin, Guard_MaskedUse, Guard_XContext_Typed) are specified in Annex C.3.A. Use those shapes; the present section is a manager‑level overview only.

#Inputs & roles (at guard time)

• TargetSlice — the specific context you are deciding for: Context, versioned Standards, environment parameters, and an explicit time selector (Γ_time).

• Typed carriers

  • ESG: the Claim quantifies over one or more Kinds (e.g., “for all vehicles in the target context …”).
  • Method–Work: the Capability declares expected input/output kinds (and possibly RoleMasks).

• Thresholds (context‑local policy):

  • Minimum F level for the Claim (if the Context gates on rigor),
  • Minimum congruence for scope bridges,
  • Minimum type‑congruence for KindBridges,
  • Evidence freshness windows (R‑lane).

• Evidence bundle (if the transition implies trust): references, dates, windows.

#Manager’s 7‑step checklist (operational)

1. Name the slice. Write the full TargetSlice/JobSlice tuple including Γ_time.
2. Check coverage. Claim/Work scope covers the slice (USM).
3. Check typed definedness. A deterministic membership check is available in this context for every kind you use (and any masks are registered).
4. Check typed compatibility. same Context: ⊑ (or mask constraints met). Cross‑context: KindBridge with CL^k ≥ c.
5. Bridge scope if needed. Scope Bridge with CL ≥ c for Cross‑context scope.
6. Apply penalties to R. Apply the scope‑bridge penalty and the kind‑bridge penalty; then check evidence freshness windows.
7. (If gated) Check F. Enforce Formality ≥ F_k for the transition.

Remember: F and G never change because of bridges; only R is penalized. AT (K0…K3) is informative and not used in guards.

#Cross‑references

• USM / A.2.6: Scope coverage, Γ_time, serial ∩, SpanUnion, Bridge+CL.
• Kind‑CAL / C.3.1–C.3.4: U.Kind, ⊑, MemberOf, RoleMask, KindBridge + CL^k.
• Formality / C.2.3: U.Formality thresholds (when ESG gates on rigor).
• Assurance / C.2.2: Freshness windows; Φ(CL) and Ψ(CL^k) penalties to R (weakest‑link on paths).

This subsection is normative for guards in ESG and Method–Work that use kinds.