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.

Correct formFrozen execution sceneBoundary

Incorrect form and why it stays silent

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

Arxo 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);

complete monitoring satisfies

Arxo 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;
}

missing policy stays undetermined

Arxo 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;
}

out-of-domain stays undetermined

Arxo 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;
}

counterexample violates

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

narrowed completeness stays undetermined

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