Check that an example is sensitive to the rule

Intention

I want to prove that the promised answer depends on the shown rule.

A behavioural witness is separated from a mere hash change: the outcome must differ, not just the bytes.

Correct formFrozen execution sceneBoundary

Incorrect form and why it stays silent

A green answer without deleting the decisive form does not yet check the pitfall.

Incorrect form

// Только eligible(p), вопрос registered(p), ожидается TRUE_ONLY.
// Правило Register забыли включить в программу.

Correct form

A self-contained witness:

Arxo Law

language "law.core" version "0.2";
package recipes.n.r13 version "0.1.0";
namespace "urn:recipe:n-package:13";

entity Person;
relation eligible(p: Person);
relation registered(p: Person);
rule Register strict { for p: Person; when eligible(p); then registered(p); }

Frozen execution scene

A local pair:

Facts	Question	Answer
eligible(p) and the Register rule	registered(p)	TRUE_ONLY
Same facts, Register cut out	registered(p)	NEITHER

Counterfactual

The sidecar cuts the full Register declaration through without. The same input becomes NEITHER; the outcome is checked, not a hash change.

Boundary

A surviving mutation does not prove equivalence, and a killed one does not prove completeness of the formalization.

Pitfall

Changing a label or a single hash does not count as behavioural detection of a mutant. Here the witness is the difference between Established and Not established, not refuted on one input.