Item 130: An intervention semantics for Robust Openness, read off the accounted state

The non-capture certificate theorems (NonCaptureCertificate.lean) quantify over a scenario: the coverage state of a concern on the actual prefix and one state per declared intervention. How a counterfactual state is produced is the external semantics, and the Lean does not model it; the wiki says the semantics is indexed by the accounted state, so that it can read the docket, the ports and the accounts. Wanted: a declared intervention class and a semantics over the accounted state that produces the scenario, with the certificate theorems (certPlus_iff_robustOpen, robustOpen_of_persistence) instantiated on at least one accounted fixture; or a stated reason the semantics belongs to the application and not to the theory.

Deliverable shape: a declared intervention class and semantics over the accounted state, with the certificate theorems instantiated on it, or a stated reason the semantics belongs to the application alone. Acceptance check: Lean green; Scenario.cf produced by the semantics on at least one accounted fixture, with certPlus_iff_robustOpen and robustOpen_of_persistence instantiated there. Context: wiki/Openness-Coverage-and-Non-Capture.md; lean/Workspace/Normativity/Contrib/NonCaptureCertificate.lean; the claim split-bill-is-robust-openness of the map.