Obligation enforcement backed

The check is obligation_enforcement_backed. Stage spec. Default-on. Severity warning. It walks every active requirement. For each cataloged checklist class it asks two questions. Is there a signal rule that lists the class, in project.signals.mappings or in a builtin pack's metadata.proof.obligations? Is there any evidence for that pair: a triple-form annotation, an authored traces.obligation_evidence cell, an evidence-profile result, or the same on a descendant linked by satisfies?

If the class is in the catalog and both answers are no, the hop warns. Finding id is orphan_enforcement:<REQ-ID>:<class>. The checklist claimed coverage. Nothing in this repo enforces or witnesses it.

proof audit --check obligation_enforcement_backed
# STK-REQ-001 obligation_checklist: [atomicity]
# catalog has atomicity. no signal mapping. no triple.
# warn: orphan_enforcement:STK-REQ-001:atomicity
# silent no-op: the catalog entry exists but nothing enforces or witnesses it

catalog_completeness only asks whether the name resolves. This hop asks whether anything backs it. Uncataloged names stay on that hop. Missing evidence depth stays on obligation_evidence_complete. A covering SYS-REQ stays on obligation_completeness.

Fix one of three ways. Add a signal rule that lists the class. Add a triple // STK-REQ-001:atomicity:nominal (or an evidence-profile result). Or disposition it if it does not apply here.

proof req edit STK-REQ-001 --suppress-obligation atomicity --reason "..."
proof req edit STK-REQ-001 --defer-obligation atomicity --reason "..." --tracking "..."
proof catalog show atomicity
proof signals list

The teaching graph is still one listed class with no rule and no witness. Add a mapping, add a triple, or disposition it. Do not treat a Jama cell as this hop. Do not treat a catalog hit as enforcement.

proof audit --check obligation_enforcement_backed --verbose
proof catalog show atomicity
proof signals list

The name hop stays on catalog completeness. The covering-child hop stays on obligation completeness. The depth hop stays on obligation evidence complete. Jama still authors. Proof vs Jama.

The hop does not write a signal mapping. It does not write the triple. Severity is warning; findings do not fail the first install unless you raise the fail level. Zero checklist items is a silent pass. A nil project is skip. A scan error is a fail, not a silent-no-op finding. Uncataloged names are not this hop. Suppressed, deferred, and delegated classes are authored dispositions, not silent. Terminal requirements are skipped. Signal backing is class-level: one mapping anywhere in the project clears every requirement that lists that class. Evidence here is presence, not depth. Opt-out is project.checks.obligation_enforcement_backed.enabled: false; that is skip, never pass. The hop does not prove the Go. We have not scored this floor against a frozen Jama pack. The loss is named, not scored.

The name hop stays on catalog completeness. The engagement stays on software correctness audit. Jama still authors.

What is obligation enforcement backed? Same question. Same URL.

Is this catalog completeness? No. That hop is whether the class name resolves. This hop is whether a resolved class has a rule or a witness. See catalog completeness.

Is this obligation completeness? No. That hop is whether each listed class has a covering SYS-REQ. See obligation completeness.

Is this obligation evidence complete? No. That hop is whether required evidence kinds exist. This hop is whether any backing exists at all. See obligation evidence complete.

Is this obligation baseline? No. That hop is whether a tag-matched class was listed or suppressed. This hop is whether a listed class has a rule or a witness. See obligation baseline.

Is this obligation delegation resolves? No. That hop is whether a named owner still carries the class. This hop is whether a listed class has a rule or a witness. See obligation delegation resolves.

Is this obligation suppression rationale? No. That hop is whether a suppress reason is still a sentence. This hop is whether a listed class has a rule or a witness. See obligation suppression rationale.

Is this obligation suppression reviewer? No. That hop is whether an error-severity suppress still carries reviewed_by. This hop is whether a listed class has a rule or a witness. See obligation suppression reviewer.

Is this obligation witness grounded? No. That hop is whether a coverage-trackable triple still executed the impl. This hop is whether a listed class has a signal or any evidence. See obligation witness grounded.

Is this code signal obligations reviewed? No. That hop is whether a fresh signal still has a listed class on the owner. This hop is the other direction. See code signal obligations reviewed.

Is this obligation profile evidence complete? No. That hop is whether a mapped profile still has a passing result file. This hop is whether a listed class has a rule or a witness. See obligation profile evidence complete.

Is this obligation decomposition complete? No. That hop is whether a listed class flowed to a satisfying child. This hop is whether a listed class has a rule or a witness. See obligation decomposition complete.

Is this spec to obligations? No. That hop compiles a shall. See spec to obligations.

Does a suppress count as backing? No. A suppress, defer, or delegate is an authored disposition. The hop skips it. It is not a silent no-op.

Does a green hop prove the Go? No. The hop does not execute a test. It does not prove the shall.

Is Proof a Jama alternative for the shall? No. Jama still authors. Proof vs Jama.