Certification Predicate

Certification Predicate

Purpose

flexo-rtm exposes two formal certification predicates: a basic predicate that ships in v0.1, and a full-assurance predicate deferred to the future topological framework. Both take the same inputs — a canonicalized RDF dataset $D$ and a scope $S$ — and return a single Boolean. The full-assurance predicate entails the basic predicate: any graph satisfying full-assurance at $S$ also satisfies basic at $S$, but not vice versa. The two predicates are layered, not competing, and they share the same rtm:satisfies verification edge as common substrate.

This page gives the formal definition of each predicate, the SPARQL/SHACL machinery that decides them, the entailment relationship, and the rationale for shipping two predicates rather than one tunable knob. See Design Spec §4.1 for the basic predicate, §4.10 for the full-assurance predicate, and §9.A.5 for the cross-cutting acceptance criteria (X1, X3) that constrain both.

Basic (v0.1) predicate

The basic predicate is the certification surface every Doors / Jama / OSLC-RM practitioner already recognizes as "the RTM is complete." It is defined entirely over the rtm:satisfies verification edge and the two coverage statistics from Traditional Forward and Backward Analysis.

Definition. Given a canonical dataset $D$ and a scope $S$:

$$\text{Basic}(D, S) \iff \text{forward%}(D, S) \geq \theta_\text{forward} ;\wedge; \text{backward%}(D, S) \geq \theta_\text{backward}$$

where the per-dimension coverage statistics, computed over the scope's induced subgraph, are:

• $\text{forward%}(D, S) = \dfrac{|{r \in R(D) \cap S : \exists a ;.; a \texttt{ rtm:satisfies } r}|}{|R(D) \cap S|}$
• $\text{backward%}(D, S) = \dfrac{|{a \in A(D) \cap S \setminus A_\text{foundational} : \exists r ;.; a \texttt{ rtm:satisfies } r}|}{|A(D) \cap S \setminus A_\text{foundational}|}$

Default thresholds. $\theta_\text{forward} = \theta_\text{backward} = 100%$. Projects MAY relax these thresholds locally; the chosen values are written into the transcript so the predicate evaluation is reproducible (per Design Spec §9.A.5 X2 replay).

SPARQL implementation. The basic predicate decomposes into two parameterized aggregate queries — one per direction — both wrapped in deterministic ordering so transcripts are byte-identical across runs (X1):

PREFIX rtm: <https://flexo-rtm.org/ns/core#>

# Forward coverage over scope ?S
SELECT (COUNT(?req) AS ?reqTotal)
       (COUNT(?covered) AS ?reqCovered) WHERE {
  ?req a rtm:Requirement ; rtm:withinScope ?S .
  OPTIONAL {
    ?art rtm:satisfies ?req ; rtm:withinScope ?S .
    BIND(?req AS ?covered)
  }
}
ORDER BY ?S

PREFIX rtm: <https://flexo-rtm.org/ns/core#>

# Backward coverage over scope ?S
SELECT (COUNT(?art) AS ?artTotal)
       (COUNT(?traced) AS ?artTraced) WHERE {
  ?art a rtm:Artifact ; rtm:withinScope ?S .
  FILTER NOT EXISTS { ?art a rtm:FoundationalArtifact . }
  OPTIONAL {
    ?art rtm:satisfies ?req .
    BIND(?art AS ?traced)
  }
}
ORDER BY ?S

The oracle records both queries and both result sets in the transcript, computes the two percentages, compares to the configured thresholds, and emits the Boolean. The full per-row enumeration is also persisted so consumers can independently re-derive the predicate from the recorded coverage statistics (X3 forbids rolling these dimensions into a single headline number — the predicate is the threshold-applied conjunction, not a smoothed grade).

What this predicate proves. Every requirement in scope has at least one satisfying artifact (no orphan requirements, gap T1), and every non-foundational artifact in scope contributes to at least one requirement (no dangling evidence, gap T2). This is the predicate a Doors or Jama team recognizes as "the RTM is complete." It runs directly against the OSLC-RM adapter's output with no additional vocabulary, no guidance vertices, no attestations, no profile composition. The oracle's certify --level=basic evaluates this predicate and nothing else.

Full-assurance (future-framework) predicate

The full-assurance predicate is the certification surface the future topological framework will expose. It conjoins the basic predicate with a topological condition $\Phi_\text{topo}$ that audits the assurance-triangle structure introduced by the deferred framework (Design Spec §4.10). It is not part of v0.1; the shapes that decide $\Phi_\text{topo}$ are scoped to the deferred capabilities D1 and D2 in Design Spec §9.A.6 and are intentionally absent from the v0.1 release gate.

Definition.

$$\text{FullAssurance}(D, S) \iff \text{Basic}(D, S) ;\wedge; \Phi_\text{topo}(D, S)$$

The topological conjunction. $\Phi_\text{topo}(D, S)$ is the conjunction of four clauses:

1. Closed assurance faces. Every non-foundational vertex in scope belongs to at least one closed assurance face: $\forall v \in (V(D) \cap S) \setminus V_\text{boundary} : \exists f \in F(D) \cap S, v \in \partial f$. See Vertices Edges Faces for the simplicial-complex semantics.
2. Named approvers on validation edges. Every Validation edge in scope carries an rtm:approvedBy IRI satisfying the v0.1 SHACL shape (sh:nodeKind sh:IRI, sh:minCount 1). This clause's SHACL shape is the same shape v0.1 already enforces on attestations (Design Spec §4.3); the future framework simply requires the named-approver presence over every Validation edge in scope.
3. Topological invariant. $V - F \leq 1$, or an alternative formulation pending the research recorded in Design Spec §9.A.6 D4. This is a purely numerical check; it is necessary but not sufficient for recursive completeness, which is why clause 4 is required.
4. No stale attestations. Every face's recorded input hash matches the current canonical hash of the inputs the face attests over: $\forall f \in F(D) \cap S : \text{hash}\text{recorded}(f) = \text{hash}\text{canonical}(\text{inputs}(f))$. Attestations whose subject inputs have mutated since the attestation was signed are stale and cause $\Phi_\text{topo}$ to fail. This clause is what makes the future-framework predicate sensitive to commit-sequence evolution.

Deferred decision machinery. Clauses 1, 3, and 4 are decided by SPARQL over the assurance-complex view (Vertices Edges Faces); clause 2 is a SHACL shape on rtm:ValidationEdge that mirrors the v0.1 rtm:AttestationShape. None of this machinery runs in v0.1. The audit gates that admit it are D1 (closed assurance triangle audit) and D2 (recursive completeness against the registry) in Design Spec §9.A.6.

Entailment relationship

$\text{FullAssurance}(D, S) \Rightarrow \text{Basic}(D, S)$ — the full-assurance predicate entails the basic predicate.

The argument is direct: rtm:satisfies is the same edge in both predicates, and every closed assurance face presupposes an rtm:satisfies edge between its Artifact and Requirement vertices. If every non-foundational vertex in scope sits on at least one closed face (clause 1 of $\Phi_\text{topo}$), then every Requirement is satisfied by at least one Artifact (forward = 100%) and every non-foundational Artifact satisfies at least one Requirement (backward = 100%). At the default thresholds, basic certification is entailed; a 100%-covered scope trivially exceeds any threshold $\leq 100%$, so the entailment holds even under relaxed thresholds.

The converse does not hold. $\text{Basic}(D, S) \not\Rightarrow \text{FullAssurance}(D, S)$ — a graph with full forward and backward coverage can fail $\Phi_\text{topo}$ on any clause: no Guidance vertices, no closed faces, missing approver IRIs, $V - F$ out of bounds, or stale attestation hashes. A user can stop at the basic predicate and hold a valid certification. Full-assurance is opt-in, not a hidden requirement.

Why two predicates (not one with a threshold)

A single tunable predicate would be cleaner in the abstract, but two predicates are the correct shape for three reasons.

First, the basic predicate matches existing RTM tooling. Doors, Jama, OSLC-RM, and three decades of practice have settled on bidirectional traceability as "the RTM is complete." Adopters get a familiar surface from their existing data, with no commitment to new vocabulary, on day one.

Second, the full-assurance predicate makes a structurally stronger claim with different vocabulary requirements. It depends on Guidance vertices, Validation edges, closed assurance faces, and a named-approver registry that does not exist in v0.1. Collapsing the two into a single graded predicate would force adopters to commit to future-framework vocabulary before the framework is built.

Third, the predicates are layered, not competing. The entailment $\text{FullAssurance} \Rightarrow \text{Basic}$ means a project can adopt the basic predicate today, accumulate the future-framework vocabulary opportunistically per Design Spec §4.2, and graduate when the framework is ready — without rewriting data. Two predicates with a clean entailment relationship encode this migration path explicitly; a single predicate with a knob does not.

Why "predicate" and not "metric"

A predicate is binary; a metric is quantitative. The certification outcome at scope $S$ is binary by design (per Design Spec §9.A.5 X1 — determinism makes the outcome a function of canonical input, and the threshold comparison produces a single Boolean). The coverage metrics — forward %, backward %, per-aspect, per-claim-type — are reported separately, per dimension, and never collapsed into a single rolled-up "% certified" headline (per Design Spec §9.A.5 X3). The predicate is the threshold-applied outcome over those metrics; the metrics themselves remain visible in the transcript and report. See Quantitative Outcomes for the metrics surface.

The split matters because audit reports must support both deterministic pass/fail and rich per-dimension diagnostics. The predicate answers "did this scope certify?"; the metrics answer "where are the gaps?". Conflating the two into one headline grade would lose the gap information practitioners need.

Scope-relativity

Both predicates are evaluated at a scope $S$, not over the whole graph. The same dataset $D$ admits many scopes, and Basic (or FullAssurance) can pass at one and fail at another. Typical pattern: a subsystem scope certifies cleanly while the full-system scope does not, because integration evidence has not yet landed.

Scopes form an algebra (see Analysis Layer Scope Algebra); the predicate is a function of the $(D, S)$ pair, and the result for Basic(D, S_1) says nothing about Basic(D, S_2). The scope IRI is recorded in the transcript so the evaluation is reproducible (X2). Scope-relativity is what makes incremental certification possible: a project can certify subsystems independently as they mature, without waiting for the full model to clear.

Cross-links

• Traditional Forward and Backward Analysis — the SPARQL implementations of forward% and backward%, and the gap codes T1 / T2 the basic predicate falsifies.
• Vertices Edges Faces — the simplicial-complex vocabulary $V$, $F$, $\partial f$ that $\Phi_\text{topo}$ ranges over.
• Quantitative Outcomes — the per-dimension metrics surface and the X3 criterion that forbids a single rolled-up grade.
• Gap Taxonomy — the gap codes (T1–T8 for the basic surface, G3–G9 deferred) that the predicates falsify when they fail.
• Analysis Layer Scope Algebra — the scope formalism the predicates are evaluated against.
• Verifiable Self-Certification — the certification artifact the predicate evaluation produces.
• Design Spec §4.1 (basic predicate), §4.10 (full-assurance / future framework), §9.A.5 (X1 determinism, X3 quantitative outcomes), §9.A.6 (D1 triangle closure, D2 recursive completeness).