docs← Back to article

Markdown for LLMs

Check that an example is sensitive to the rule

The source Markdown for this article. Copy it into your assistant or download it as a text file.

Download this articlePlain text ↗
# 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.

## Incorrect form and why it stays silent

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

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

## Correct form

A self-contained witness:

```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.