# Prove maintenance compliance

## Intention

I want to distinguish complete observation of the window from one positive fact.

Completeness must cover the duty-holder and the end of the window.

## Incorrect form and why it stays silent

```text title="Incorrect form"
// done(p) после окончания окна достаточно для SATISFIED.
```

The applicable closure must cover exactly this duty-holder and the whole window. Without a policy a positive fact leaves UNDETERMINED.

## Correct form

```law
language "law.core" version "0.2";
package recipes.zh.r07 version "0.1.0";
namespace "urn:recipe:zh-violation:07";

entity Person;
relation enrolled(p: Person);
relation done(p: Person);
relation monitored(p: Person);
rule Primary defeasible { for p: Person; when enrolled(p);
    then duty Main { bearer p; maintain done(p) during [@2026-09-01, @2026-09-10]; };
}
closure Monitoring { predicate done; domain monitored; snapshot MONITOR_2026;
    complete_as_of @2026-09-11T00:00:00+05:00;
    derive_explicit_negative true;
    effective [@2026-01-01, @2027-01-01);
}
```

## Frozen execution scene

| Facts and snapshot | Question | Answer |
|---|---|---|
| complete observation; 2026-09-13 | `positions()` | `position(Main, SATISFIED);` |
| without a policy; 2026-09-13 | `positions()` | `position(Main, UNDETERMINED);` |
| outside the domain; 2026-09-13 | `positions()` | `position(Main, UNDETERMINED);` |
| counterexample; 2026-09-13 | `positions()` | `position(Main, VIOLATED);` |

```law
test "complete monitoring satisfies" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-30T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert enrolled(entity_ref("urn:recipe:zh-violation:07:p")); assert done(entity_ref("urn:recipe:zh-violation:07:p")); assert monitored(entity_ref("urn:recipe:zh-violation:07:p"));
    }
    evaluate positions();
    expect position(Main, SATISFIED);
    expect evaluation_status == COMPUTED;
}
```

```law
test "missing policy stays undetermined" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-30T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert enrolled(entity_ref("urn:recipe:zh-violation:07:p")); assert done(entity_ref("urn:recipe:zh-violation:07:p")); assert monitored(entity_ref("urn:recipe:zh-violation:07:p"));
    }
    evaluate positions();
    expect position(Main, UNDETERMINED);
    expect evaluation_status == COMPUTED;
}
```

```law
test "out-of-domain stays undetermined" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-30T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert enrolled(entity_ref("urn:recipe:zh-violation:07:p")); assert done(entity_ref("urn:recipe:zh-violation:07:p"));
    }
    evaluate positions();
    expect position(Main, UNDETERMINED);
    expect evaluation_status == COMPUTED;
}
```

```law
test "counterexample violates" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-30T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert enrolled(entity_ref("urn:recipe:zh-violation:07:p")); assert monitored(entity_ref("urn:recipe:zh-violation:07:p")); assert not done(entity_ref("urn:recipe:zh-violation:07:p"));
    }
    evaluate positions();
    expect position(Main, VIOLATED);
    expect evaluation_status == COMPUTED;
}
```

Completeness is dated at noon of the last day of the window instead of the start of the next day: coverage of the whole window is not proven.

```law
test "narrowed completeness stays undetermined" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-30T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert enrolled(entity_ref("urn:recipe:zh-violation:07:p")); assert done(entity_ref("urn:recipe:zh-violation:07:p")); assert monitored(entity_ref("urn:recipe:zh-violation:07:p"));
    }
    evaluate positions();
    expect position(Main, UNDETERMINED);
    expect evaluation_status == COMPUTED;
}
```

```python
>>> import runpy
>>> check = runpy.run_path("docs/recipes/zh-violation/resources/check.py")
>>> check["check_variant"](https://github.com/arxohq/law/blob/master/docs/recipes/zh-violation/7)
'Ж7: контрфактуал подтверждён; lawc = lawref'
```

## Counterfactual

Diagnostic mutation `snapshot MONITOR_2026;` → ``: LDC-E1307. Semantic differences are pinned as separate scenes.

## Boundary

The path of an applicable closure policy is shown. A monitoring certificate and binding adjudication are other grounds; an arbitrary certificate label does not become them. On the last day of the window a conservative snapshot needs a separate completeness justification.