C.3.A:3 - Shared outcome model
All guards obey these invariants.
- Exact declarations. A kind designator never substitutes for the exact
KindSignatureedition needed by the use. - 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, checks admissibility, and evaluates the four-input judgment only for an admissible request.
- Admissibility, then three classification values. Check candidate and slice admissibility under the pinned declarations before any C.3.2 or C.3.4 judgment below. An inadmissible request gives
not-applicable; no judgment is formed. For admissible inputs,truemeans the criterion is known to hold;falsemeans it is known to fail;unknownmeans the evaluation cannot settle because evidence or a declared dependency is unavailable. - Separate guard disposition. A guard returns an action disposition such as allow or refuse. An inadmissible request causes refusal without a classification judgment. Both
falseandunknownnormally cause fail-closed refusal, but the guard MUST preserve which classification value it consumed. - Scope separation. Scope coverage is a USM predicate over a named slice. It does not classify the candidate or repair kind compatibility. Scope translation enters only when exact local senses require it under A.2.6; a changed locality or scheme alone does not trigger it. The Scope Bridge shorthand below denotes the obtaining F.9 Bridge, while a separate affirmative C.2.1 claim states this translation’s direction, rule, and permitted loss. Reliance uses the current A.10 disposition or, when a named assurance claim is current, a B.3 result supporting this same use.
- Bridge separation. An obtaining KindBridge relation connects exact, independently identified distinct source and target kinds when its directional correspondence predicate holds under C.3.3. Its separate bridge assertion supplies mapping,
CL^k, loss, evidence, definedness, and admitted use; neither object creates a target kind, signature, or judgment. A locality change alone supplies no such relation. Same-kind reuse selects the receiving declaration edition and, when a candidate is current, a fresh receiving judgment. - R-only consequences. Justified scope- and kind-bridge consequences affect R only. They do not change F, G, or classification truth.