docs← Back to article

Markdown for LLMs

Establish the absence of a registry record

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

Download this articlePlain text ↗
# Establish the absence of a registry record

## Intention

I want to treat the absence of a licence as a negative fact only inside a complete registry.

## Incorrect form and why it stays silent

Without a snapshot the closure is rejected; a date instead of a completeness instant also does not work.

```text title="Incorrect form"
closure Registry { predicate licensed; domain registered; complete_as_of @2026-09-13; }
```

## Correct form

```law
language "law.core" version "0.2";
package recipes.v.r01 version "0.1.0";
namespace "urn:recipe:v-negation:01";

entity Person;
relation registered(p: Person);
relation licensed(p: Person);
relation pair_domain(p: Person, q: Person);
closure Registry {
    predicate licensed;
    domain registered;
    snapshot REGISTRY_2026;
    complete_as_of @2026-09-13T00:00:00+05:00;
    derive_explicit_negative true;
    effective [@2026-01-01, @2027-01-01);
}
```

## Frozen execution scene

| Facts | Question | Answer |
|---|---|---|
| registered(a), no record | licensed(a) | FALSE_ONLY |
| registered(a), licensed(a) | licensed(a) | TRUE_ONLY |
| outside the domain | licensed(a) | NEITHER |
| registered(a), legal_time 2027-01-01 | licensed(a) | NEITHER |
| registered(a), without Registry | licensed(a) | NEITHER |

```law
test "absent record denies license" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert registered(entity_ref("urn:recipe:v-negation:01:a"));
    }
    evaluate truth(licensed(entity_ref("urn:recipe:v-negation:01:a")));
    expect truth_status == FALSE_ONLY;

}
```

```law
test "present record grants license" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert registered(entity_ref("urn:recipe:v-negation:01:a"));
        assert licensed(entity_ref("urn:recipe:v-negation:01:a"));
    }
    evaluate truth(licensed(entity_ref("urn:recipe:v-negation:01:a")));
    expect truth_status == TRUE_ONLY;

}
```

```law
test "out-of-domain entity stays unknown" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }

    }
    evaluate truth(licensed(entity_ref("urn:recipe:v-negation:01:a")));
    expect truth_status == NEITHER;

}
```

```law
test "closed effective window yields neither" {
    given {
        context {
            legal_time @2027-01-01;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert registered(entity_ref("urn:recipe:v-negation:01:a"));
    }
    evaluate truth(licensed(entity_ref("urn:recipe:v-negation:01:a")));
    expect truth_status == NEITHER;

}
```

## Counterfactual

Mutations remove snapshot, replace Instant with a date, and substitute a binary relation for domain: E1307, E1307, E2114. Without the closure at all, evaluates gets NEITHER.

## Boundary

Tuples are closed, not the whole world. The snapshot name in this witness is a policy identifier; the registry's external bytes are not loaded. In a real case, completeness and provenance are supplied by the snapshot holder.

## Pitfall

Absence of a debt without a producer of the negative yields NEITHER; closure fixes the answer. Closure allows any matching arity, not only the unary form.