C.3.A:4.1 - 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:
   • 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
   • for a required directional correspondence between independently identified distinct kinds, 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 subkind 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.